Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14626 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (165 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (112 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7292 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (761 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (250 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (390 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (84 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3144 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (126 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2221 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (53 entries) |

## B (variable)

BaseSetMulDef.gT [in fingroup]BaseSetMulProp.gT [in fingroup]

BasicSetTheory.T [in finset]

Basic_commutator_properties.LeftRightComm.j [in commutator]

Basic_commutator_properties.RightComm.i [in commutator]

Basic_commutator_properties.LeftComm.i [in commutator]

Basic_commutator_properties.LeftRightComm.cxz [in commutator]

Basic_commutator_properties.LeftRightComm.x [in commutator]

Basic_commutator_properties.RightComm.x [in commutator]

Basic_commutator_properties.LeftComm.x [in commutator]

Basic_commutator_properties.LeftRightComm.i [in commutator]

Basic_commutator_properties.RightComm.cyz [in commutator]

Basic_commutator_properties.LeftComm.cxz [in commutator]

Basic_commutator_properties.LeftRightComm.cyz [in commutator]

Basic_commutator_properties.gT [in commutator]

Basic_commutator_properties.LeftRightComm.y [in commutator]

Basic_commutator_properties.RightComm.y [in commutator]

Basic_commutator_properties.LeftComm.y [in commutator]

BigBool.I [in bigop]

BigBool.P [in bigop]

BigOps.aop [in finset]

BigOps.I [in finset]

BigOps.idx [in finset]

BigOps.J [in finset]

BigOps.op [in finset]

BigOps.R [in finset]

BigProp.idx [in bigop]

BigProp.op1 [in bigop]

BigProp.op2 [in bigop]

BigProp.Pb [in bigop]

BigProp.Pb_idx [in bigop]

BigProp.Pb_op1 [in bigop]

BigProp.Pb_eq_op [in bigop]

BigProp.R [in bigop]

BigRel.idx1 [in bigop]

BigRel.idx2 [in bigop]

BigRel.op1 [in bigop]

BigRel.op2 [in bigop]

BigRel.Pr [in bigop]

BigRel.Pr_idx [in bigop]

BigRel.Pr_rel [in bigop]

BigRel.R1 [in bigop]

BigRel.R2 [in bigop]

BigSetOps.I [in finset]

BigSetOps.T [in finset]

BijectionsTheory.A [in ssrfun]

BijectionsTheory.B [in ssrfun]

BijectionsTheory.C [in ssrfun]

BijectionsTheory.f [in ssrfun]

BijectionsTheory.h [in ssrfun]

Bijections.A [in ssrfun]

Bijections.B [in ssrfun]

Bijections.bijf [in ssrfun]

Bijections.f [in ssrfun]

BooleanAlternative.a [in ssrbool]

BooleanAlternative.bP [in ssrbool]

BooleanAlternative.T [in ssrbool]

BoolIf.A [in ssrbool]

BoolIf.B [in ssrbool]

BoolIf.b [in ssrbool]

BoolIf.f [in ssrbool]

BoolIf.vF [in ssrbool]

BoolIf.vT [in ssrbool]

BoolIf.x [in ssrbool]

Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14626 entries) |

Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (165 entries) |

Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (112 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7292 entries) |

Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (761 entries) |

Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (250 entries) |

Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (390 entries) |

Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (84 entries) |

Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3144 entries) |

Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (126 entries) |

Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |

Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2221 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (53 entries) |