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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |

## B

baseFinGroupType [abbreviation, in groups]BaseFinGroupType [abbreviation, in groups]

BasicSetTheory [section, in finset]

BasicSetTheory.T [variable, in finset]

before_find [lemma, in seq]

behead [definition, in seq]

behead_map [lemma, in seq]

behead_tuple [definition, in tuple]

behead_tupleP [lemma, in tuple]

belast [definition, in seq]

belast_cat [lemma, in seq]

belast_map [lemma, in seq]

belast_rcons [lemma, in seq]

belast_tuple [definition, in tuple]

belast_tupleP [lemma, in tuple]

bezoutl [lemma, in div]

bezoutr [lemma, in div]

bezout_rec [definition, in div]

bigA_distr_big [lemma, in bigops]

bigA_distr_bigA [lemma, in bigops]

bigA_distr_big_dep [lemma, in bigops]

bigcapP [lemma, in finset]

bigcapsP [lemma, in finset]

bigcap_group [definition, in groups]

bigcap_inf [lemma, in finset]

bigcap_min [lemma, in finset]

bigcap_setU [lemma, in finset]

bigcupP [lemma, in finset]

bigcupsP [lemma, in finset]

bigcup_disjoint [lemma, in finset]

bigcup_max [lemma, in finset]

bigcup_setU [lemma, in finset]

bigcup_sup [lemma, in finset]

bigD1 [lemma, in bigops]

bigID [lemma, in bigops]

bigop [abbreviation, in bigops]

BigOps [section, in finset]

bigops [library]

BigOps.alaw [variable, in finset]

BigOps.I [variable, in finset]

BigOps.J [variable, in finset]

BigOps.law [variable, in finset]

BigOps.nil [variable, in finset]

BigOps.R [variable, in finset]

bigprodGE [lemma, in groups]

bigprodGEgen [lemma, in groups]

BigProp [section, in bigops]

BigProp.idx [variable, in bigops]

BigProp.op1 [variable, in bigops]

BigProp.op2 [variable, in bigops]

BigProp.Pb [variable, in bigops]

BigProp.Pb_eq_op [variable, in bigops]

BigProp.Pb_idx [variable, in bigops]

BigProp.Pb_op1 [variable, in bigops]

BigProp.R [variable, in bigops]

BigRel [section, in bigops]

BigRel.idx1 [variable, in bigops]

BigRel.idx2 [variable, in bigops]

BigRel.op1 [variable, in bigops]

BigRel.op2 [variable, in bigops]

BigRel.Pr [variable, in bigops]

BigRel.Pr_idx [variable, in bigops]

BigRel.Pr_rel [variable, in bigops]

BigRel.R1 [variable, in bigops]

BigRel.R2 [variable, in bigops]

BigSetOps [section, in finset]

BigSetOps.I [variable, in finset]

BigSetOps.T [variable, in finset]

bigU [lemma, in bigops]

big1 [lemma, in bigops]

big1_eq [lemma, in bigops]

big1_seq [lemma, in bigops]

big_addn [lemma, in bigops]

big_add1 [lemma, in bigops]

big_cat [lemma, in bigops]

big_catl [lemma, in bigops]

big_catr [lemma, in bigops]

big_cat_nat [lemma, in bigops]

big_cat_nested [lemma, in bigops]

big_cond_seq [lemma, in bigops]

big_cons [lemma, in bigops]

big_const [lemma, in bigops]

big_const_nat [lemma, in bigops]

big_const_ord [lemma, in bigops]

big_const_seq [lemma, in bigops]

big_distrl [lemma, in bigops]

big_distrr [lemma, in bigops]

big_distr_big [lemma, in bigops]

big_distr_big_dep [lemma, in bigops]

big_filter [lemma, in bigops]

big_filter_cond [lemma, in bigops]

big_geq [lemma, in bigops]

big_hasC [lemma, in bigops]

big_ltn [lemma, in bigops]

big_ltn_cond [lemma, in bigops]

big_map [lemma, in bigops]

big_mkcond [lemma, in bigops]

big_mkord [lemma, in bigops]

big_morph [lemma, in bigops]

big_nat1 [lemma, in bigops]

big_nat_recl [lemma, in bigops]

big_nat_recr [lemma, in bigops]

big_nat_widen [lemma, in bigops]

big_nil [lemma, in bigops]

big_nth [lemma, in bigops]

big_ord0 [lemma, in bigops]

big_ord_narrow [lemma, in bigops]

big_ord_narrow_cond [lemma, in bigops]

big_ord_narrow_cond_leq [lemma, in bigops]

big_ord_narrow_leq [lemma, in bigops]

big_ord_recl [lemma, in bigops]

big_ord_recr [lemma, in bigops]

big_ord_widen [lemma, in bigops]

big_ord_widen_cond [lemma, in bigops]

big_ord_widen_leq [lemma, in bigops]

big_pred0 [lemma, in bigops]

big_pred0_eq [lemma, in bigops]

big_pred1 [lemma, in bigops]

big_pred1_eq [lemma, in bigops]

big_prop [lemma, in bigops]

big_prop_seq [lemma, in bigops]

big_rel [lemma, in bigops]

big_rel_seq [lemma, in bigops]

big_seq1 [lemma, in bigops]

big_setD1 [lemma, in finset]

big_setID [lemma, in finset]

big_setU1 [lemma, in finset]

big_set0 [lemma, in finset]

big_set1 [lemma, in finset]

big_split [lemma, in bigops]

big_split_ord [lemma, in bigops]

big_sumType [lemma, in bigops]

big_trivIset [lemma, in finset]

big_uniq [lemma, in bigops]

Bijections [section, in ssrfun]

BijectionsTheory [section, in ssrfun]

BijectionsTheory.A [variable, in ssrfun]

BijectionsTheory.B [variable, in ssrfun]

BijectionsTheory.C [variable, in ssrfun]

BijectionsTheory.f [variable, in ssrfun]

BijectionsTheory.h [variable, in ssrfun]

Bijections.A [variable, in ssrfun]

Bijections.B [variable, in ssrfun]

Bijections.bijf [variable, in ssrfun]

Bijections.f [variable, in ssrfun]

bijective [definition, in ssrfun]

bijective_in [definition, in ssrbool]

bijective_on [definition, in ssrbool]

bij_can_bij [lemma, in ssrfun]

bij_can_eq [lemma, in ssrfun]

bij_can_sym [lemma, in ssrfun]

bij_comp [lemma, in ssrfun]

bij_eq [lemma, in eqtype]

bij_inj [lemma, in ssrfun]

bin [definition, in binomial]

binE [lemma, in binomial]

binn [lemma, in binomial]

binomial [library]

binS [lemma, in binomial]

bin0 [lemma, in binomial]

bin_fact [lemma, in binomial]

bin_gt0 [lemma, in binomial]

bin_nat_eqMixin [definition, in ssrnat]

bin_nat_eqType [definition, in ssrnat]

bin_of_nat [definition, in ssrnat]

bin_of_natK [lemma, in ssrnat]

bin_of_number [projection, in ssrnat]

bin_rec [definition, in binomial]

bin_small [lemma, in binomial]

bin_sub [lemma, in binomial]

bitseq [definition, in seq]

bitseq_choiceType [definition, in choice]

bitseq_countType [definition, in choice]

bitseq_eqType [definition, in seq]

bitseq_predType [definition, in seq]

block_mx [definition, in matrix]

block_mxEll [lemma, in matrix]

block_mxElr [lemma, in matrix]

block_mxEul [lemma, in matrix]

block_mxEur [lemma, in matrix]

block_mxKll [lemma, in matrix]

block_mxKlr [lemma, in matrix]

block_mxKul [lemma, in matrix]

block_mxKur [lemma, in matrix]

block_mx0 [lemma, in matrix]

BoolIf [section, in ssrbool]

BoolIf.A [variable, in ssrbool]

BoolIf.B [variable, in ssrbool]

BoolIf.b [variable, in ssrbool]

BoolIf.f [variable, in ssrbool]

BoolIf.vF [variable, in ssrbool]

BoolIf.vT [variable, in ssrbool]

BoolIf.x [variable, in ssrbool]

bool_choiceMixin [definition, in choice]

bool_choiceType [definition, in choice]

bool_countMixin [definition, in choice]

bool_countType [definition, in choice]

bool_enumP [lemma, in fintype]

bool_eqMixin [definition, in eqtype]

bool_eqType [definition, in eqtype]

bool_finMixin [definition, in fintype]

bool_finType [definition, in fintype]

bool_irrelevance [lemma, in eqtype]

bool_pickleK [lemma, in choice]

bump [definition, in fintype]

bumpK [lemma, in fintype]

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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |