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) |

## C

C [abbreviation, in center]cAA [definition, in maximal]

cancel [definition, in ssrfun]

cancel_index_extremal_groups [lemma, in extremal]

CanChoiceMixin [definition, in choice]

CanCountMixin [definition, in choice]

CanEqMixin [definition, in eqtype]

CanFinMixin [definition, in fintype]

canF_eq [lemma, in fintype]

canF_RL [lemma, in fintype]

canF_LR [lemma, in fintype]

canF_sym [lemma, in fintype]

canF_invF [lemma, in fintype]

canLR [lemma, in ssrfun]

canLR_on [lemma, in ssrbool]

canLR_in [lemma, in ssrbool]

canRL [lemma, in ssrfun]

canRL_on [lemma, in ssrbool]

canRL_in [lemma, in ssrbool]

can_inj [lemma, in ssrfun]

can_imset_pre [lemma, in finset]

can_eq [lemma, in eqtype]

can_comp [lemma, in ssrfun]

can_in_inj [lemma, in ssrbool]

can_pcan [lemma, in ssrfun]

can_in_eq [lemma, in eqtype]

can2_in_imset_pre [lemma, in finset]

can2_imset_pre [lemma, in finset]

can2_mem_pmap [lemma, in seq]

can2_eq [lemma, in eqtype]

capfv [lemma, in vector]

capmx [definition, in mxalgebra]

capmxA [lemma, in mxalgebra]

capmxC [lemma, in mxalgebra]

capmxE [lemma, in mxalgebra]

capmxMr [lemma, in mxalgebra]

capmxS [lemma, in mxalgebra]

capmxSl [lemma, in mxalgebra]

capmxSr [lemma, in mxalgebra]

capmxT [lemma, in mxalgebra]

capmx_idPl [lemma, in mxalgebra]

capmx_diff [lemma, in mxalgebra]

capmx_witnessP [definition, in mxalgebra]

capmx_idPr [lemma, in mxalgebra]

capmx_key [lemma, in mxalgebra]

capmx_nopP [definition, in mxalgebra]

capmx_def [definition, in mxalgebra]

capmx_nop [definition, in mxalgebra]

capmx_normP [definition, in mxalgebra]

capmx_norm_eq [definition, in mxalgebra]

capmx_witness [definition, in mxalgebra]

capmx_norm [definition, in mxalgebra]

capmx_compl [lemma, in mxalgebra]

capmx_gen [definition, in mxalgebra]

capmx_eq_norm [definition, in mxalgebra]

capmx_nop_id [definition, in mxalgebra]

capmx_comoid [definition, in mxalgebra]

capmx_monoid [definition, in mxalgebra]

capmx_module [lemma, in mxrepresentation]

capmx_subSocle [lemma, in mxrepresentation]

capmx0 [lemma, in mxalgebra]

capmx1 [lemma, in mxalgebra]

capTmx [lemma, in mxalgebra]

capv [definition, in vector]

capvA [lemma, in vector]

capvC [lemma, in vector]

capvf [lemma, in vector]

capvKl [lemma, in vector]

capvKr [lemma, in vector]

capvS [lemma, in vector]

capvSl [lemma, in vector]

capvSr [lemma, in vector]

capvv [lemma, in vector]

capv_compl [lemma, in vector]

capv_mx2vsr [lemma, in vector]

capv_vs2mx [lemma, in vector]

capv_diff [lemma, in vector]

capv_mx2vsl [lemma, in vector]

capv_mx2vs [lemma, in vector]

capv_comoid [definition, in vector]

capv_monoid [definition, in vector]

capv0 [lemma, in vector]

cap_eqmx [lemma, in mxalgebra]

cap0mx [lemma, in mxalgebra]

cap0v [lemma, in vector]

cap1mx [lemma, in mxalgebra]

cardC [lemma, in fintype]

CardCosetpre [section, in quotient]

CardCosetpre.G [variable, in quotient]

CardCosetpre.gT [variable, in quotient]

CardCosetpre.H [variable, in quotient]

CardCosetpre.K [variable, in quotient]

CardCosetpre.L [variable, in quotient]

CardCosetpre.M [variable, in quotient]

cardC1 [lemma, in fintype]

CardDef [module, in fintype]

CardDefSig [module, in fintype]

CardDefSig.card [axiom, in fintype]

CardDefSig.cardEdef [axiom, in fintype]

CardDef.card [definition, in fintype]

CardDef.cardEdef [definition, in fintype]

cardD1 [lemma, in fintype]

cardD1x [lemma, in bigop]

cardE [lemma, in fintype]

CardFunImage [section, in fintype]

CardFunImage [section, in finset]

CardFunImage.aT [variable, in finset]

CardFunImage.aT2 [variable, in finset]

CardFunImage.D [variable, in finset]

CardFunImage.D2 [variable, in finset]

CardFunImage.f [variable, in fintype]

CardFunImage.f [variable, in finset]

CardFunImage.f2 [variable, in finset]

CardFunImage.g [variable, in finset]

CardFunImage.injf [variable, in fintype]

CardFunImage.rT [variable, in finset]

CardFunImage.T [variable, in fintype]

CardFunImage.T' [variable, in fintype]

CardGL [section, in mxalgebra]

CardGL.F [variable, in mxalgebra]

cardG_gt0_reduced [definition, in fingroup]

cardG_gt0 [lemma, in fingroup]

cardG_gt1 [lemma, in fingroup]

cardID [lemma, in fintype]

cardIg_divn [lemma, in fingroup]

cardJg [lemma, in fingroup]

cardMg_divn [lemma, in fingroup]

cardMg_TI [lemma, in fingroup]

CardMorphism [section, in quotient]

CardMorphism.aT [variable, in quotient]

CardMorphism.D [variable, in quotient]

CardMorphism.f [variable, in quotient]

CardMorphism.rT [variable, in quotient]

cardsC [lemma, in finset]

cardsCs [lemma, in finset]

cardsC1 [lemma, in finset]

cardsD1 [lemma, in finset]

cardsE [lemma, in finset]

cardSg [lemma, in fingroup]

cardSg_cyclic [lemma, in cyclic]

cardsID [lemma, in finset]

CardSig [section, in fintype]

CardSig.P [variable, in fintype]

CardSig.T [variable, in fintype]

cardsT [lemma, in finset]

cardsUI [lemma, in finset]

cardsU1 [lemma, in finset]

cardsX [lemma, in finset]

cards_eq0 [lemma, in finset]

cards0 [lemma, in finset]

cards0_eq [lemma, in finset]

cards1 [lemma, in finset]

cards1P [lemma, in finset]

cards2 [lemma, in finset]

cardT [lemma, in fintype]

cardUI [lemma, in fintype]

cardU1 [lemma, in fintype]

cardX [lemma, in fintype]

card_p3group_extraspecial [lemma, in maximal]

card_orbit1 [lemma, in action]

card_p1Elem [lemma, in abelian]

card_ltn_sorted_tuples [lemma, in binomial]

card_def [abbreviation, in fintype]

card_p2group_abelian [lemma, in sylow]

card_le1_trivg [lemma, in fingroup]

card_option [lemma, in fintype]

card_rcoset [lemma, in fingroup]

card_lcosets [lemma, in fingroup]

card_unit [lemma, in fintype]

card_pfamily [lemma, in finfun]

card_Alt [lemma, in alt]

card_orbit_in [lemma, in action]

card_preim [lemma, in fintype]

card_Fp [lemma, in zmodp]

card_setact [lemma, in action]

card_family [lemma, in finfun]

card_sum [lemma, in fintype]

card_linear_irr [lemma, in mxrepresentation]

card_sorted_tuples [lemma, in binomial]

card_dihedral [lemma, in extremal]

card_isog [lemma, in morphism]

card_classes_abelian [lemma, in action]

card_conjugates [lemma, in action]

card_mem_repr [lemma, in fingroup]

card_ord [lemma, in fintype]

card_semidihedral [lemma, in extremal]

card_unlock [definition, in fintype]

card_cosetpre [lemma, in quotient]

card_uniqP [lemma, in fintype]

card_ord_partitions [lemma, in binomial]

card_modular_group [lemma, in extremal]

card_matrix [lemma, in matrix]

card_pnElem [lemma, in abelian]

card_Syl_mod [lemma, in sylow]

card_im_injm [lemma, in morphism]

card_rVabelem [lemma, in mxabelem]

card_morphim [lemma, in quotient]

card_inj_ffuns_on [lemma, in binomial]

card_ext_dihedral [lemma, in extremal]

card_center_extraspecial [lemma, in maximal]

card_homg [lemma, in quotient]

card_abelem_rV [lemma, in mxabelem]

card_Zp [lemma, in zmodp]

card_size [lemma, in fintype]

card_Sym [lemma, in alt]

card_DnQ [lemma, in extraspecial]

card_injm [lemma, in morphism]

card_orbit [lemma, in action]

card_subcent_extraspecial [lemma, in maximal]

card_Syl_dvd [lemma, in sylow]

card_uniq_tuple [lemma, in primitive_action]

card_partial_ord_partitions [lemma, in binomial]

card_image [lemma, in fintype]

card_pgroup [lemma, in pgroup]

card_prod [lemma, in fintype]

card_tagged [lemma, in fintype]

card_p1Elem_p2Elem [lemma, in abelian]

card_orbit_stab [lemma, in action]

card_draws [lemma, in binomial]

card_pffun_on [lemma, in finfun]

card_irr [lemma, in mxrepresentation]

card_uniq_tuples [lemma, in binomial]

card_imset [lemma, in finset]

card_inj_ffuns [lemma, in binomial]

card_partition [lemma, in finset]

card_perm [lemma, in perm]

card_gt0P [lemma, in fintype]

card_GL_2 [lemma, in mxalgebra]

card_uniform_partition [lemma, in finset]

card_pX1p2n [lemma, in extraspecial]

card_preimset [lemma, in finset]

card_GL [lemma, in mxalgebra]

card_codom [lemma, in fintype]

card_quotient_subnorm [lemma, in quotient]

card_Aut_cyclic [lemma, in cyclic]

card_seq_sub [lemma, in fintype]

card_type [abbreviation, in fintype]

card_sig [lemma, in fintype]

card_Hall [lemma, in pgroup]

card_rowg [lemma, in mxabelem]

card_2dihedral [lemma, in extremal]

card_ffun [lemma, in finfun]

card_in_image [lemma, in fintype]

card_quotient [lemma, in quotient]

card_morphpre [lemma, in quotient]

card_gt0 [lemma, in finset]

card_extraspecial [lemma, in maximal]

card_in_imset [lemma, in finset]

card_Aut_cycle [lemma, in cyclic]

card_tuple [lemma, in tuple]

card_quaternion [lemma, in extremal]

card_p1Elem_pnElem [lemma, in abelian]

card_ffun_on [lemma, in finfun]

card_isog8_extraspecial [lemma, in extraspecial]

card_Syl [lemma, in sylow]

card_units_Zp [lemma, in zmodp]

card_powerset [lemma, in finfun]

card_lcoset [lemma, in fingroup]

card_orbit_in_stab [lemma, in action]

card_sub [lemma, in fintype]

card_GL_1 [lemma, in mxalgebra]

card_bool [lemma, in fintype]

card_invg [lemma, in fingroup]

card_pX1p2 [lemma, in extraspecial]

card0 [lemma, in fintype]

card0_eq [lemma, in fintype]

card1 [lemma, in fintype]

card1_trivg [lemma, in fingroup]

card2 [lemma, in fintype]

CartesianProd [section, in finset]

CartesianProd.A1 [variable, in finset]

CartesianProd.A2 [variable, in finset]

CartesianProd.fT1 [variable, in finset]

CartesianProd.fT2 [variable, in finset]

castmx [definition, in matrix]

castmxE [lemma, in matrix]

castmxK [lemma, in matrix]

castmxKV [lemma, in matrix]

castmx_id [lemma, in matrix]

castmx_comp [lemma, in matrix]

castmx_sym [lemma, in matrix]

castmx_const [lemma, in matrix]

cast_ordK [lemma, in fintype]

cast_col_mx [lemma, in matrix]

cast_ord [definition, in fintype]

cast_ord_comp [lemma, in fintype]

cast_ord_inj [lemma, in fintype]

cast_row_mx [lemma, in matrix]

cast_ordKV [lemma, in fintype]

cast_ord_proof [lemma, in fintype]

cast_ord_id [lemma, in fintype]

cat [definition, in seq]

catA [lemma, in seq]

catrev [definition, in seq]

cats0 [lemma, in seq]

cats1 [lemma, in seq]

cat_nseq [lemma, in seq]

cat_tuple [definition, in tuple]

cat_cons [lemma, in seq]

cat_take_drop [lemma, in seq]

cat_rcons [lemma, in seq]

cat_monoid [definition, in bigop]

cat_uniq [lemma, in seq]

cat_tupleP [lemma, in tuple]

cat0s [lemma, in seq]

cat1s [lemma, in seq]

Cauchy [lemma, in pgroup]

Cayley_repr [definition, in action]

Cayley_isog [lemma, in action]

Cayley_Hamilton [lemma, in mxpoly]

Cayley_isom [lemma, in action]

centC [lemma, in fingroup]

Center [section, in center]

center [definition, in center]

center [library]

centerC [lemma, in center]

centerP [lemma, in center]

center_cprod [lemma, in center]

center_idP [lemma, in center]

center_abelian [lemma, in center]

center_nil_eq1 [lemma, in nilpotent]

center_aut_extraspecial [lemma, in maximal]

center_char [lemma, in center]

center_prod [lemma, in center]

center_kquo_cyclic [lemma, in mxrepresentation]

center_mx [definition, in mxalgebra]

center_bigdprod [lemma, in center]

center_mx_sub [lemma, in mxalgebra]

center_bigcprod [lemma, in center]

center_special_abelem [lemma, in maximal]

center_ncprod [lemma, in center]

center_ncprod0 [lemma, in center]

center_pgFun [definition, in center]

center_gFun [definition, in center]

center_igFun [definition, in center]

center_group [definition, in center]

center_normal [lemma, in center]

center_sub [lemma, in center]

center_mxP [lemma, in mxalgebra]

center_dprod [lemma, in center]

Center.gT [variable, in center]

Center.Injm [section, in center]

Center.Injm.D [variable, in center]

Center.Injm.f [variable, in center]

Center.Injm.injf [variable, in center]

Center.Injm.rT [variable, in center]

center1 [lemma, in center]

centgmx [definition, in mxrepresentation]

centgmxP [lemma, in mxrepresentation]

centgmx_map [lemma, in mxrepresentation]

centgmx_hom [lemma, in mxrepresentation]

centI [lemma, in fingroup]

centJ [lemma, in fingroup]

centM [lemma, in fingroup]

centP [lemma, in fingroup]

Central [section, in gseries]

centralised [definition, in fingroup]

centraliser [definition, in fingroup]

centraliser_group [definition, in fingroup]

centralises [definition, in fingroup]

centrals_nil [lemma, in nilpotent]

central_product [definition, in gproduct]

central_central_factor [lemma, in gseries]

central_factor_central [lemma, in gseries]

central_factor [definition, in gseries]

Central.G [variable, in gseries]

Central.gT [variable, in gseries]

centS [lemma, in fingroup]

centsC [lemma, in fingroup]

centsP [lemma, in fingroup]

centsS [lemma, in fingroup]

centSS [lemma, in fingroup]

cents_norm [lemma, in fingroup]

cents_cycle [lemma, in fingroup]

cents1 [lemma, in fingroup]

centU [lemma, in fingroup]

centY [lemma, in fingroup]

cent_mx_ideal [lemma, in mxalgebra]

cent_sub [lemma, in fingroup]

cent_gen [lemma, in fingroup]

cent_set1 [lemma, in fingroup]

cent_normal [lemma, in fingroup]

cent_semiregular [lemma, in frobenius]

cent_rowP [lemma, in mxalgebra]

cent_classP [lemma, in fingroup]

cent_mx_scalar_abs_irr [lemma, in mxrepresentation]

cent_mx_fun [definition, in mxalgebra]

cent_mx [definition, in mxalgebra]

cent_norm [lemma, in fingroup]

cent_joinEr [lemma, in fingroup]

cent_mxP [lemma, in mxalgebra]

cent_mx_fun_is_linear [lemma, in mxalgebra]

cent_semiprime [lemma, in frobenius]

cent_mx_fun_linear [definition, in mxalgebra]

cent_mx_fun_additive [definition, in mxalgebra]

cent_joinEl [lemma, in fingroup]

cent_cycle [lemma, in fingroup]

cent_mx_ring [lemma, in mxalgebra]

cent1C [lemma, in fingroup]

cent1E [lemma, in fingroup]

cent1id [lemma, in fingroup]

cent1P [lemma, in fingroup]

cent1T [lemma, in fingroup]

cent1_extraspecial_maximal [lemma, in maximal]

cent11T [lemma, in fingroup]

CH [abbreviation, in center]

ChangeOfField [section, in mxrepresentation]

ChangeOfField.aF [variable, in mxrepresentation]

ChangeOfField.f [variable, in mxrepresentation]

ChangeOfField.G [variable, in mxrepresentation]

ChangeOfField.gT [variable, in mxrepresentation]

ChangeOfField.OneRepresentation [section, in mxrepresentation]

ChangeOfField.OneRepresentation.n [variable, in mxrepresentation]

ChangeOfField.OneRepresentation.rG [variable, in mxrepresentation]

ChangeOfField.rF [variable, in mxrepresentation]

ChangeOfRing [section, in mxrepresentation]

ChangeOfRing.aR [variable, in mxrepresentation]

ChangeOfRing.f [variable, in mxrepresentation]

ChangeOfRing.G [variable, in mxrepresentation]

ChangeOfRing.gT [variable, in mxrepresentation]

ChangeOfRing.OneRepresentation [section, in mxrepresentation]

ChangeOfRing.OneRepresentation.n [variable, in mxrepresentation]

ChangeOfRing.OneRepresentation.rG [variable, in mxrepresentation]

ChangeOfRing.rR [variable, in mxrepresentation]

characteristic [definition, in automorphism]

Characteristicity [section, in automorphism]

Characteristicity.gT [variable, in automorphism]

charI [lemma, in automorphism]

CharInjm [section, in automorphism]

CharInjm.aT [variable, in automorphism]

CharInjm.D [variable, in automorphism]

CharInjm.f [variable, in automorphism]

CharInjm.injf [variable, in automorphism]

CharInjm.rT [variable, in automorphism]

charM [lemma, in automorphism]

charMgen [lemma, in automorphism]

charP [lemma, in automorphism]

CharPoly [section, in mxpoly]

CharPoly.A [variable, in mxpoly]

CharPoly.n [variable, in mxpoly]

CharPoly.R [variable, in mxpoly]

charR [lemma, in commutator]

CharSimple [section, in maximal]

charsimple [definition, in maximal]

charsimpleP [lemma, in maximal]

charsimple_dprod [lemma, in maximal]

charsimple_solvable [lemma, in maximal]

CharSimple.gT [variable, in maximal]

char_normal_trans [lemma, in automorphism]

char_Fp_0 [lemma, in zmodp]

char_norm [lemma, in automorphism]

char_refl [lemma, in automorphism]

char_sub [lemma, in automorphism]

char_poly_trace [lemma, in mxpoly]

char_poly_det [lemma, in mxpoly]

char_injm [lemma, in automorphism]

char_poly_monic [lemma, in mxpoly]

char_normal [lemma, in automorphism]

char_Zp [lemma, in zmodp]

char_norms [lemma, in automorphism]

char_trans [lemma, in automorphism]

char_poly [definition, in mxpoly]

char_from_quotient [lemma, in quotient]

char_Fp [lemma, in zmodp]

char_norm_trans [lemma, in automorphism]

char_poly_mx [definition, in mxpoly]

char1 [lemma, in automorphism]

Chiefs [section, in gseries]

Chiefs.gT [variable, in gseries]

chief_series_exists [lemma, in gseries]

chief_factor_minnormal [lemma, in gseries]

chief_factor [definition, in gseries]

chinese [definition, in div]

Chinese [section, in div]

chinese_modl [lemma, in div]

chinese_modr [lemma, in div]

chinese_modlr [lemma, in div]

chinese_remainder [lemma, in div]

Chinese.co_m12 [variable, in div]

Chinese.m1 [variable, in div]

Chinese.m2 [variable, in div]

Choice [module, in choice]

choice [library]

ChoiceTheory [section, in choice]

ChoiceTheory.SubChoice [section, in choice]

ChoiceTheory.SubChoice.P [variable, in choice]

ChoiceTheory.SubChoice.sT [variable, in choice]

ChoiceTheory.T [variable, in choice]

Choice.base [projection, in choice]

Choice.CanMixin2 [definition, in choice]

Choice.Class [constructor, in choice]

Choice.class [definition, in choice]

Choice.ClassDef [section, in choice]

Choice.ClassDef.cT [variable, in choice]

Choice.ClassDef.T [variable, in choice]

Choice.class_of [record, in choice]

Choice.clone [definition, in choice]

Choice.correct [definition, in choice]

Choice.eqType [definition, in choice]

Choice.eq_xchoose [projection, in choice]

Choice.eq_nat_xchoose [lemma, in choice]

Choice.eq_pcan_xchoose [lemma, in choice]

Choice.Exports.ChoiceMixin [abbreviation, in choice]

Choice.Exports.ChoiceType [abbreviation, in choice]

Choice.Exports.choiceType [abbreviation, in choice]

Choice.extensional [definition, in choice]

Choice.mixin [projection, in choice]

Choice.Mixin [section, in choice]

Choice.Mixin [constructor, in choice]

Choice.mixin_of [record, in choice]

Choice.Mixin.T [variable, in choice]

Choice.mixin0 [definition, in choice]

Choice.natMixin [definition, in choice]

Choice.nat_xchooseP [lemma, in choice]

Choice.Pack [constructor, in choice]

Choice.pack [definition, in choice]

Choice.PcanMixin [section, in choice]

Choice.PcanMixin [definition, in choice]

Choice.PcanMixin.f [variable, in choice]

Choice.PcanMixin.fK [variable, in choice]

Choice.PcanMixin.f' [variable, in choice]

Choice.PcanMixin.m [variable, in choice]

Choice.PcanMixin.sT [variable, in choice]

Choice.PcanMixin.T [variable, in choice]

Choice.PcanMixin.Xfun [section, in choice]

Choice.PcanMixin.Xfun.sP [variable, in choice]

Choice.PcanMixin.Xfun.xsP [variable, in choice]

Choice.pcan_xchoose [definition, in choice]

Choice.pcan_xchooseP [lemma, in choice]

Choice.pcan_xchoose_proof [lemma, in choice]

Choice.pcan_xchoose_sig [lemma, in choice]

Choice.sort [projection, in choice]

Choice.type [record, in choice]

Choice.xchoose [projection, in choice]

Choice.xchooseP [projection, in choice]

Choice.xfun [definition, in choice]

choose [definition, in choice]

chooseP [lemma, in choice]

choose_id [lemma, in choice]

CK [abbreviation, in center]

class [definition, in fingroup]

classes [definition, in fingroup]

classes1 [lemma, in fingroup]

classGidl [lemma, in fingroup]

classGidr [lemma, in fingroup]

classG_eq1 [lemma, in fingroup]

classg_base_free [lemma, in mxrepresentation]

classg_base_center [lemma, in mxrepresentation]

classg_base [definition, in mxrepresentation]

classically [definition, in ssrbool]

classicP [lemma, in ssrbool]

classic_imply [lemma, in ssrbool]

classic_bind [lemma, in ssrbool]

classic_EM [lemma, in ssrbool]

classic_pick [lemma, in ssrbool]

classM [lemma, in fingroup]

classS [lemma, in fingroup]

class_supportEl [lemma, in fingroup]

class_support [definition, in fingroup]

class_support_normG [lemma, in fingroup]

class_transr [lemma, in fingroup]

class_sym [lemma, in fingroup]

class_transl [lemma, in fingroup]

class_set1 [lemma, in fingroup]

class_supportEr [lemma, in fingroup]

class_trans [lemma, in fingroup]

class_supportM [lemma, in fingroup]

class_support_id [lemma, in fingroup]

class_formula [lemma, in action]

class_lcoset [lemma, in fingroup]

class_subG [lemma, in fingroup]

class_supportD1 [lemma, in fingroup]

class_normG [lemma, in fingroup]

class_sub_norm [lemma, in fingroup]

class_supportGidr [lemma, in fingroup]

class_support_set1l [lemma, in fingroup]

class_refl [lemma, in fingroup]

class_supportGidl [lemma, in fingroup]

class_support_set1r [lemma, in fingroup]

class_support_subG [lemma, in fingroup]

class_support_sub_norm [lemma, in fingroup]

class_rcoset [lemma, in fingroup]

class1g [lemma, in fingroup]

class1G [lemma, in fingroup]

Clifford_astab [lemma, in mxrepresentation]

Clifford_rank_components [lemma, in mxrepresentation]

Clifford_is_action [lemma, in mxrepresentation]

Clifford_basis [lemma, in mxrepresentation]

Clifford_rstabs_simple [lemma, in mxrepresentation]

Clifford_component_basis [lemma, in mxrepresentation]

Clifford_iso2 [lemma, in mxrepresentation]

Clifford_simple [lemma, in mxrepresentation]

Clifford_Socle1 [lemma, in mxrepresentation]

Clifford_componentJ [lemma, in mxrepresentation]

Clifford_action [definition, in mxrepresentation]

Clifford_hom [lemma, in mxrepresentation]

Clifford_astab1 [lemma, in mxrepresentation]

Clifford_iso [lemma, in mxrepresentation]

Clifford_atrans [lemma, in mxrepresentation]

Clifford_act [definition, in mxrepresentation]

clone_pred [definition, in ssrbool]

clone_subType [definition, in eqtype]

clone_action [definition, in action]

clone_morphism [definition, in morphism]

clone_group [definition, in fingroup]

clone_groupAction [definition, in action]

closed [definition, in fingraph]

ClosedField [module, in ssralg]

closed_connect [lemma, in fingraph]

closure [definition, in fingraph]

Closure [section, in fingraph]

closure_closed [lemma, in fingraph]

Closure.e [variable, in fingraph]

Closure.He [variable, in fingraph]

Closure.T [variable, in fingraph]

CodeSeq [module, in choice]

CodeSeq.Nat.code [definition, in choice]

CodeSeq.Nat.codeK [lemma, in choice]

CodeSeq.Nat.decode [definition, in choice]

CodeSeq.Nat.decodeK [lemma, in choice]

CodeSeq.Nat.decode_rec [definition, in choice]

CodeSeq.Seq2.code [definition, in choice]

CodeSeq.Seq2.codeK [lemma, in choice]

CodeSeq.Seq2.decode [definition, in choice]

CodeSeq.Seq2.decodeK [lemma, in choice]

CodeSeq.Seq2.pad [definition, in choice]

CodeSeq.Seq2.padding [definition, in choice]

CodeSeq.Seq2.padKl [lemma, in choice]

CodeSeq.Seq2.padKr [lemma, in choice]

CodeSeq.Seq2.Seq2 [section, in choice]

CodeSeq.Seq2.Seq2.T [variable, in choice]

CodeSeq.Seq2.strip [definition, in choice]

CodeSeq.Seq2.stripK [lemma, in choice]

codom [definition, in fintype]

codom_f [lemma, in fintype]

coefC [lemma, in poly]

coefK [lemma, in poly]

coefX [lemma, in poly]

coef_cons [lemma, in poly]

coef_opp_poly [lemma, in poly]

coef_Cmul [lemma, in poly]

coef_rVpoly_ord [lemma, in mxpoly]

coef_opp [lemma, in poly]

coef_mul_poly [lemma, in poly]

coef_rVpoly [lemma, in mxpoly]

coef_map [lemma, in poly]

coef_deriv [lemma, in poly]

coef_mul_poly_rev [lemma, in poly]

coef_Xn [lemma, in poly]

coef_derivn [lemma, in poly]

coef_Poly [lemma, in poly]

coef_nderivn [lemma, in poly]

coef_mulX [lemma, in poly]

coef_scaler [lemma, in poly]

coef_add_poly [lemma, in poly]

coef_poly [lemma, in poly]

coef_natmul [lemma, in poly]

coef_negmul [lemma, in poly]

coef_Xn_mul [lemma, in poly]

coef_add [lemma, in poly]

coef_mulC [lemma, in poly]

coef_mulXn [lemma, in poly]

coef_mul [lemma, in poly]

coef_sum [lemma, in poly]

coef_sub [lemma, in poly]

coef_mul_rev [lemma, in poly]

coef_Xmul [lemma, in poly]

coef0 [lemma, in poly]

coef1 [lemma, in poly]

cofactor [definition, in matrix]

cofactor_tr [lemma, in matrix]

cofactor_map_mx [lemma, in matrix]

coGA' [definition, in hall]

cokermx [definition, in mxalgebra]

cokermx_eq0 [lemma, in mxalgebra]

col [definition, in matrix]

colKl [lemma, in matrix]

colKr [lemma, in matrix]

colP [lemma, in matrix]

col_base [definition, in mxalgebra]

col_mxKd [lemma, in matrix]

col_mxKu [lemma, in matrix]

col_const [lemma, in matrix]

col_id [lemma, in matrix]

col_leq_rank [lemma, in mxalgebra]

col_eq [lemma, in matrix]

col_ebase [definition, in mxalgebra]

col_mx_sub [lemma, in mxalgebra]

col_mxA [lemma, in matrix]

col_perm [definition, in matrix]

col_mxEd [lemma, in matrix]

col_mxEu [lemma, in matrix]

col_mxAx [definition, in matrix]

col_base_full [lemma, in mxalgebra]

col_row_permC [lemma, in matrix]

col_mx_const [lemma, in matrix]

col_ebase_unit [lemma, in mxalgebra]

col_perm1 [lemma, in matrix]

col_permM [lemma, in matrix]

col_perm_linear [definition, in matrix]

col_linear [definition, in matrix]

col_perm_additive [definition, in matrix]

col_additive [definition, in matrix]

col_mx0 [lemma, in matrix]

col_mx [definition, in matrix]

col_perm_const [lemma, in matrix]

col_col_mx [lemma, in matrix]

col_permE [lemma, in matrix]

col' [definition, in matrix]

col'Kl [lemma, in matrix]

col'Kr [lemma, in matrix]

col'_eq [lemma, in matrix]

col'_linear [definition, in matrix]

col'_additive [definition, in matrix]

col'_col_mx [lemma, in matrix]

col'_const [lemma, in matrix]

col0 [lemma, in matrix]

Combinations [section, in binomial]

ComMatrix [section, in matrix]

ComMatrix.AssocLeft [section, in matrix]

ComMatrix.AssocLeft.m [variable, in matrix]

ComMatrix.AssocLeft.n [variable, in matrix]

ComMatrix.AssocLeft.p [variable, in matrix]

ComMatrix.LinMulRow [section, in matrix]

ComMatrix.LinMulRow.m [variable, in matrix]

ComMatrix.LinMulRow.n [variable, in matrix]

ComMatrix.MatrixAlgType [section, in matrix]

ComMatrix.MatrixAlgType.n' [variable, in matrix]

ComMatrix.R [variable, in matrix]

commg [definition, in fingroup]

commgAC [lemma, in commutator]

commgC [lemma, in fingroup]

commGC [lemma, in fingroup]

commgCV [lemma, in fingroup]

commgEl [lemma, in fingroup]

commgEr [lemma, in fingroup]

commgg [lemma, in fingroup]

commgMJ [lemma, in commutator]

commgMR [lemma, in commutator]

commgP [lemma, in fingroup]

commgS [lemma, in fingroup]

commgSS [lemma, in fingroup]

commgV [lemma, in commutator]

commgVg [lemma, in fingroup]

commgX [lemma, in commutator]

commgXg [lemma, in fingroup]

commgXVg [lemma, in fingroup]

commg_subI [lemma, in commutator]

commg_normal [lemma, in commutator]

commg_normSr [lemma, in commutator]

commg_subr [lemma, in commutator]

commg_norml [lemma, in commutator]

commg_set [definition, in fingroup]

commg_normSl [lemma, in commutator]

commg_subl [lemma, in commutator]

commg_sub [lemma, in commutator]

commg_normr [lemma, in commutator]

commg_norm [lemma, in commutator]

commg1 [lemma, in fingroup]

commG1 [lemma, in commutator]

commG1P [lemma, in fingroup]

commg1_sym [lemma, in fingroup]

commMG [lemma, in commutator]

commMgJ [lemma, in commutator]

commMGr [lemma, in commutator]

commMgR [lemma, in commutator]

commr_polyXn [lemma, in poly]

commr_polyX [lemma, in poly]

commr_rmorph [definition, in poly]

commSg [lemma, in fingroup]

commutative [definition, in ssrfun]

commutator [definition, in fingroup]

commutator [library]

Commutator_properties.gT [variable, in commutator]

commutator_group [definition, in fingroup]

Commutator_properties [section, in commutator]

commute [definition, in fingroup]

commuteM [lemma, in fingroup]

commuteV [lemma, in fingroup]

commuteX [lemma, in fingroup]

commuteX2 [lemma, in fingroup]

commute_refl [lemma, in fingroup]

commute_sym [lemma, in fingroup]

commute1 [lemma, in fingroup]

commVg [lemma, in commutator]

commXg [lemma, in commutator]

commXXg [lemma, in commutator]

comm_group_setP [lemma, in fingroup]

comm_norm_cent_cent [lemma, in commutator]

comm_subG [lemma, in fingroup]

comm_sub_max_pgroup [lemma, in pgroup]

comm_joingE [lemma, in fingroup]

comm1G [lemma, in commutator]

comm1g [lemma, in fingroup]

comm3G1P [lemma, in commutator]

comp [abbreviation, in ssrfun]

comp [abbreviation, in ssrfun]

CompAct [section, in action]

CompAct.aT [variable, in action]

CompAct.B [variable, in action]

CompAct.D [variable, in action]

CompAct.f [variable, in action]

CompAct.gT [variable, in action]

CompAct.rT [variable, in action]

CompAct.to [variable, in action]

comparable [definition, in eqtype]

comparableClass [definition, in eqtype]

ComparableType [section, in eqtype]

ComparableType.Hcompare [variable, in eqtype]

ComparableType.T [variable, in eqtype]

compareb [definition, in eqtype]

CompareNatEq [constructor, in ssrnat]

CompareNatGt [constructor, in ssrnat]

CompareNatLt [constructor, in ssrnat]

compareP [lemma, in eqtype]

compare_nat [inductive, in ssrnat]

CompImage [section, in vector]

CompImage.K [variable, in vector]

CompImage.V [variable, in vector]

CompImage.W [variable, in vector]

CompImage.Z [variable, in vector]

complements_to_in [definition, in gproduct]

complete_unitmx [lemma, in mxalgebra]

complgC [lemma, in gproduct]

CompLinearApp [section, in vector]

CompLinearApp.R [variable, in vector]

CompLinearApp.V [variable, in vector]

CompLinearApp.W [variable, in vector]

CompLinearApp.Z [variable, in vector]

complmx [definition, in mxalgebra]

complP [lemma, in gproduct]

complv [definition, in vector]

compl_p'Hall [lemma, in pgroup]

compl_pHall [lemma, in pgroup]

compo [abbreviation, in jordanholder]

ComPolyCompose [section, in poly]

ComPolyCompose.R [variable, in poly]

component_mx_id [lemma, in mxrepresentation]

component_mx_module [lemma, in mxrepresentation]

component_mx_isoP [lemma, in mxrepresentation]

component_socle [lemma, in mxrepresentation]

component_mx_semisimple [lemma, in mxrepresentation]

component_mx_iso [lemma, in mxrepresentation]

component_mx_disjoint [lemma, in mxrepresentation]

component_mx_key [lemma, in mxrepresentation]

component_mx_expr [abbreviation, in mxrepresentation]

component_mx [definition, in mxrepresentation]

component_mx_def [lemma, in mxrepresentation]

component_mxE [lemma, in mxrepresentation]

Composition [section, in ssrfun]

CompositionSeries [section, in jordanholder]

CompositionSeries.gT [variable, in jordanholder]

Composition.A [variable, in ssrfun]

Composition.B [variable, in ssrfun]

Composition.C [variable, in ssrfun]

comps [definition, in jordanholder]

compsP [lemma, in jordanholder]

comps_cons [lemma, in jordanholder]

compU [abbreviation, in mxrepresentation]

comp_reprGLm [lemma, in mxabelem]

comp_morphM [lemma, in morphism]

comp_act [definition, in action]

comp_lapp_addl [lemma, in vector]

comp_actE [lemma, in action]

comp_is_groupAction [lemma, in action]

comp_morphism [definition, in morphism]

comp_lapp1 [lemma, in vector]

comp_lappE [lemma, in vector]

comp_lapp [definition, in vector]

comp_1lapp [lemma, in vector]

comp_groupAction [definition, in action]

comp_action [definition, in action]

comp_lappA [lemma, in vector]

comp_lapp_addr [lemma, in vector]

comp_is_action [lemma, in action]

ComRing [module, in ssralg]

ComRing [module, in finalg]

ComUnitRing [module, in ssralg]

ComUnitRing [module, in finalg]

com_polyX [lemma, in poly]

com_poly [definition, in poly]

com_poly1 [lemma, in poly]

com_poly0 [lemma, in poly]

com_coef [definition, in poly]

com_coef_poly [lemma, in poly]

conform_castmx [lemma, in matrix]

conform_mx [definition, in matrix]

conform_mx_id [lemma, in matrix]

congr_big_nat [lemma, in bigop]

congr_group [lemma, in fingroup]

congr_subv [lemma, in vector]

congr_big [lemma, in bigop]

congr_subg [lemma, in fingroup]

congr1 [definition, in ssrfun]

congr2 [definition, in ssrfun]

conjCg [lemma, in fingroup]

conjDg [lemma, in fingroup]

conjD1g [lemma, in fingroup]

conjg [definition, in fingroup]

conjgC [lemma, in fingroup]

conjgCV [lemma, in fingroup]

conjgE [lemma, in fingroup]

conjGid [lemma, in fingroup]

conjgK [lemma, in fingroup]

conjgKV [lemma, in fingroup]

conjgM [lemma, in fingroup]

conjgm [definition, in automorphism]

conjgmE [lemma, in automorphism]

conjgm_morphism [definition, in automorphism]

conjG_is_action [lemma, in action]

conjG_group [definition, in fingroup]

conjg_Rmul [lemma, in commutator]

conjg_mulR [lemma, in commutator]

conjG_action [definition, in action]

conjg_preim [lemma, in fingroup]

conjg_fixP [lemma, in fingroup]

conjg_is_groupAction [lemma, in action]

conjg_inj [lemma, in fingroup]

conjg_groupAction [definition, in action]

conjg_action [definition, in action]

conjg_set1 [lemma, in fingroup]

conjg1 [lemma, in fingroup]

conjIg [lemma, in fingroup]

conjJg [lemma, in fingroup]

conjMg [lemma, in fingroup]

conjRg [lemma, in fingroup]

conjSg [lemma, in fingroup]

conjsgE [lemma, in fingroup]

conjsgK [lemma, in fingroup]

conjsgKV [lemma, in fingroup]

conjsgM [lemma, in fingroup]

conjsg_inj [lemma, in fingroup]

conjsg_action [definition, in action]

conjsg1 [lemma, in fingroup]

conjsMg [lemma, in fingroup]

conjsRg [lemma, in fingroup]

conjs1g [lemma, in fingroup]

conjUg [lemma, in fingroup]

conjugate [definition, in fingroup]

conjugates [definition, in fingroup]

conjugatesS [lemma, in fingroup]

conjugates_set1 [lemma, in fingroup]

conjugates_conj [lemma, in fingroup]

ConjugationMorphism [section, in automorphism]

ConjugationMorphism.G [variable, in automorphism]

ConjugationMorphism.gT [variable, in automorphism]

conjVg [lemma, in fingroup]

conjXg [lemma, in fingroup]

conjYg [lemma, in fingroup]

conj_subG [lemma, in fingroup]

conj_mx_irr [lemma, in mxrepresentation]

conj_mx_faithful [lemma, in mxrepresentation]

conj_aut_morphism [definition, in automorphism]

conj_autE [lemma, in automorphism]

conj_aut [definition, in automorphism]

conj_isog [lemma, in automorphism]

conj_aut_morphM [lemma, in automorphism]

conj1g [lemma, in fingroup]

Connect [section, in fingraph]

connect [definition, in fingraph]

connectP [lemma, in fingraph]

connect_trans [lemma, in fingraph]

connect_closed [lemma, in fingraph]

connect_sub [lemma, in fingraph]

connect_root [lemma, in fingraph]

connect_sym [definition, in fingraph]

Connect.e [variable, in fingraph]

Connect.T [variable, in fingraph]

connect0 [lemma, in fingraph]

connect1 [lemma, in fingraph]

Cons [constructor, in seq]

cons [abbreviation, in seq]

ConsPred [abbreviation, in pgroup]

constant [definition, in seq]

constantP [lemma, in seq]

constant_nseq [lemma, in seq]

constt [definition, in pgroup]

consttC [lemma, in pgroup]

consttJ [lemma, in pgroup]

consttM [lemma, in pgroup]

consttNK [lemma, in pgroup]

consttV [lemma, in pgroup]

consttX [lemma, in pgroup]

constt_p_elt [lemma, in pgroup]

constt1 [lemma, in pgroup]

constt1P [lemma, in pgroup]

const_mx [definition, in matrix]

const_mx_is_additive [lemma, in matrix]

const_mx_additive [definition, in matrix]

cons_tuple [definition, in tuple]

cons_uniq [lemma, in seq]

cons_pfactor [definition, in prime]

contra [lemma, in ssrbool]

contraFF [lemma, in ssrbool]

contraFN [lemma, in ssrbool]

contraFT [lemma, in ssrbool]

contraL [lemma, in ssrbool]

contraLR [lemma, in ssrbool]

contraNeq [lemma, in eqtype]

contraNF [lemma, in ssrbool]

contraNN [definition, in ssrbool]

contraNneq [lemma, in eqtype]

contraNT [definition, in ssrbool]

Contrapositives [section, in eqtype]

Contrapositives.b [variable, in eqtype]

Contrapositives.T [variable, in eqtype]

Contrapositives.x [variable, in eqtype]

Contrapositives.y [variable, in eqtype]

contraR [lemma, in ssrbool]

contraT [lemma, in ssrbool]

contraTeq [lemma, in eqtype]

contraTF [lemma, in ssrbool]

contraTN [definition, in ssrbool]

contraTneq [lemma, in eqtype]

contraTT [definition, in ssrbool]

contra_orbit [lemma, in action]

coord [definition, in vector]

coord_basis [lemma, in vector]

coord_sumE [lemma, in vector]

coord_span [lemma, in vector]

coord_is_linear [lemma, in vector]

coord_linear [definition, in vector]

copid_mx [definition, in matrix]

copid_mx_id [lemma, in matrix]

coprime [definition, in div]

coprimegS [lemma, in fingroup]

coprimenP [lemma, in div]

coprimenS [lemma, in div]

coprimen1 [lemma, in div]

coprimeP [lemma, in div]

coprimePn [lemma, in div]

coprimeSg [lemma, in fingroup]

coprimeSn [lemma, in div]

coprime_cent_mulG [lemma, in hall]

coprime_egcdn [lemma, in div]

coprime_Hall_trans [lemma, in hall]

coprime_morphl [lemma, in quotient]

coprime_cardMg [lemma, in fingroup]

coprime_p'group [lemma, in pgroup]

coprime_sdprod_Hall [lemma, in pgroup]

coprime_modl [lemma, in div]

coprime_pcoreC [lemma, in pgroup]

coprime_Hall_exists [lemma, in hall]

coprime_morph [lemma, in quotient]

coprime_Hall_subset [lemma, in hall]

coprime_dvdl [lemma, in div]

coprime_mulGp_Hall [lemma, in pgroup]

coprime_expr [lemma, in div]

coprime_norm_cent [lemma, in hall]

coprime_quotient_cent [lemma, in hall]

coprime_index_mulG [lemma, in fingroup]

coprime_mull [lemma, in div]

coprime_pexpl [lemma, in div]

coprime_pexpr [lemma, in div]

coprime_dvdr [lemma, in div]

coprime_expl [lemma, in div]

coprime_norm_quotient_cent [lemma, in hall]

coprime_comm_pcore [lemma, in hall]

coprime_morphr [lemma, in quotient]

coprime_partC [lemma, in prime]

coprime_mulG_setI_norm [lemma, in sylow]

coprime_TIg [lemma, in fingroup]

coprime_has_primes [lemma, in prime]

coprime_sym [lemma, in div]

coprime_mulr [lemma, in div]

coprime_modr [lemma, in div]

coprime_pi' [lemma, in prime]

coprime_abel_cent_TI [lemma, in finmodule]

coprime_mulpG_Hall [lemma, in pgroup]

coprime1n [lemma, in div]

CormenLUP [section, in matrix]

CormenLUP.F [variable, in matrix]

cormen_lup_lower [lemma, in matrix]

cormen_lup [definition, in matrix]

cormen_lup_upper [lemma, in matrix]

cormen_lup_correct [lemma, in matrix]

cormen_lup_perm [lemma, in matrix]

cormen_lup_detL [lemma, in matrix]

Coset [constructor, in quotient]

coset [definition, in quotient]

CosetOfGroupTheory [section, in quotient]

CosetOfGroupTheory.gT [variable, in quotient]

CosetOfGroupTheory.H [variable, in quotient]

CosetOfGroupTheory.Injective [section, in quotient]

CosetOfGroupTheory.Injective.G [variable, in quotient]

CosetOfGroupTheory.Injective.nHG [variable, in quotient]

CosetOfGroupTheory.Injective.tiHG [variable, in quotient]

CosetOfGroupTheory.InverseImage [section, in quotient]

CosetOfGroupTheory.InverseImage.G [variable, in quotient]

CosetOfGroupTheory.InverseImage.Kbar [variable, in quotient]

CosetOfGroupTheory.InverseImage.nHG [variable, in quotient]

cosetP [lemma, in quotient]

cosetpreK [lemma, in quotient]

cosetpreM [lemma, in quotient]

cosetpreSK [lemma, in quotient]

cosetpre_cent1 [lemma, in quotient]

cosetpre_normal [lemma, in quotient]

cosetpre_cent1s [lemma, in quotient]

cosetpre_cents [lemma, in quotient]

cosetpre_maximal [lemma, in gseries]

cosetpre_subcent [lemma, in quotient]

cosetpre_maximal_eq [lemma, in gseries]

cosetpre_cent [lemma, in quotient]

cosetpre_set1_coset [lemma, in quotient]

cosetpre_proper [lemma, in quotient]

cosetpre_set1 [lemma, in quotient]

cosetpre_subcent1 [lemma, in quotient]

cosetpre_gen [lemma, in quotient]

cosetpre1 [lemma, in quotient]

Cosets [section, in quotient]

Cosets.A [variable, in quotient]

Cosets.gT [variable, in quotient]

Cosets.Q [variable, in quotient]

coset_inv [definition, in quotient]

coset_eqMixin [definition, in quotient]

coset_range_mul [lemma, in quotient]

coset_one [definition, in quotient]

coset_morphism [definition, in quotient]

coset_groupType [definition, in quotient]

coset_baseGroupType [definition, in quotient]

coset_subFinType [definition, in quotient]

coset_finType [definition, in quotient]

coset_subCountType [definition, in quotient]

coset_countType [definition, in quotient]

coset_choiceType [definition, in quotient]

coset_eqType [definition, in quotient]

coset_subType [definition, in quotient]

coset_reprK [lemma, in quotient]

coset_morphM [lemma, in quotient]

coset_idr [lemma, in quotient]

coset_countMixin [definition, in quotient]

coset_mul [definition, in quotient]

coset_kerl [lemma, in quotient]

coset_mulP [lemma, in quotient]

coset_transversal [definition, in finmodule]

coset_id [lemma, in quotient]

coset_default [lemma, in quotient]

coset_of [record, in quotient]

coset_of_groupMixin [definition, in quotient]

coset_kerr [lemma, in quotient]

coset_one_proof [lemma, in quotient]

coset_oneP [lemma, in quotient]

coset_mem [lemma, in quotient]

coset_finMixin [definition, in quotient]

coset_norm [lemma, in quotient]

coset_splitting_field [lemma, in mxrepresentation]

coset_invP [lemma, in quotient]

coset_choiceMixin [definition, in quotient]

coset_range [definition, in quotient]

coset_range_inv [lemma, in quotient]

coset1 [lemma, in quotient]

coset1_injm [lemma, in quotient]

count [definition, in seq]

Countable [module, in choice]

CountableTheory [section, in choice]

CountableTheory.T [variable, in choice]

Countable.base [projection, in choice]

Countable.ChoiceMixin [definition, in choice]

Countable.choiceType [definition, in choice]

Countable.class [definition, in choice]

Countable.Class [constructor, in choice]

Countable.ClassDef [section, in choice]

Countable.ClassDef.cT [variable, in choice]

Countable.ClassDef.T [variable, in choice]

Countable.class_of [record, in choice]

Countable.clone [definition, in choice]

Countable.EqMixin [definition, in choice]

Countable.eqType [definition, in choice]

Countable.Exports.CountChoiceMixin [abbreviation, in choice]

Countable.Exports.CountMixin [abbreviation, in choice]

Countable.Exports.CountType [abbreviation, in choice]

Countable.Exports.countType [abbreviation, in choice]

Countable.Mixin [constructor, in choice]

Countable.mixin [projection, in choice]

Countable.mixin_of [record, in choice]

Countable.Pack [constructor, in choice]

Countable.pack [definition, in choice]

Countable.pickle [projection, in choice]

Countable.pickleK [projection, in choice]

Countable.PickleSeq [section, in choice]

Countable.PickleSeq.p [variable, in choice]

Countable.PickleSeq.pK [variable, in choice]

Countable.PickleSeq.T [variable, in choice]

Countable.PickleSeq.u [variable, in choice]

Countable.pickle_seqK [lemma, in choice]

Countable.pickle_seq [definition, in choice]

Countable.sort [projection, in choice]

Countable.type [record, in choice]

Countable.unpickle [projection, in choice]

Countable.unpickle_seq [definition, in choice]

count_predC [lemma, in seq]

count_pred0 [lemma, in seq]

count_mem_uniq [lemma, in seq]

count_predT [lemma, in seq]

count_cat [lemma, in seq]

count_logn_dprod_cycle [lemma, in abelian]

count_uniq_mem [lemma, in seq]

count_size [lemma, in seq]

count_map [lemma, in seq]

count_predUI [lemma, in seq]

count_filter [lemma, in seq]

cover [definition, in finset]

cover_at [definition, in finset]

cover_imset [lemma, in finset]

cover_at_mem [lemma, in finset]

cover_at_eq [lemma, in finset]

cover_setI [lemma, in finset]

cpairg1 [definition, in center]

cpairg1_dom [lemma, in center]

cpairg1_center [lemma, in center]

cpair_center_id [lemma, in center]

cpair1g [definition, in center]

cpair1g_dom [lemma, in center]

cpair1g_center [lemma, in center]

cprod [abbreviation, in gproduct]

cprod [abbreviation, in gproduct]

cprodA [lemma, in gproduct]

CprodBy [section, in center]

CprodBy.ExtCprodm [section, in center]

CprodBy.ExtCprodm.cfHK [variable, in center]

CprodBy.ExtCprodm.eq_fHK [variable, in center]

CprodBy.ExtCprodm.fH [variable, in center]

CprodBy.ExtCprodm.fK [variable, in center]

CprodBy.ExtCprodm.rT [variable, in center]

CprodBy.gTH [variable, in center]

CprodBy.gTK [variable, in center]

CprodBy.gz [variable, in center]

CprodBy.H [variable, in center]

CprodBy.Isomorphism [section, in center]

CprodBy.Isomorphism.AutZHfull [variable, in center]

CprodBy.Isomorphism.defG [variable, in center]

CprodBy.Isomorphism.G [variable, in center]

CprodBy.Isomorphism.GH [variable, in center]

CprodBy.Isomorphism.GK [variable, in center]

CprodBy.Isomorphism.isoGH [variable, in center]

CprodBy.Isomorphism.isoGK [variable, in center]

CprodBy.Isomorphism.rT [variable, in center]

CprodBy.Isomorphism.ziGHK [variable, in center]

CprodBy.isoZ [variable, in center]

CprodBy.K [variable, in center]

cprodC [lemma, in gproduct]

cprodE [lemma, in gproduct]

cprodEY [lemma, in gproduct]

cprodg1 [lemma, in gproduct]

cprodm [definition, in gproduct]

cprodmE [lemma, in gproduct]

cprodmEl [lemma, in gproduct]

cprodmEr [lemma, in gproduct]

cprodm_morphism [definition, in gproduct]

cprodm_actf [lemma, in gproduct]

cprodm_norm [lemma, in gproduct]

cprodm_sub [lemma, in gproduct]

cprodP [lemma, in gproduct]

cprod_abelaw [definition, in gproduct]

cprod_law [definition, in gproduct]

cprod_center_id [lemma, in center]

cprod_abelem [lemma, in abelian]

cprod_ntriv [lemma, in gproduct]

cprod_modr [lemma, in gproduct]

cprod_nil [lemma, in nilpotent]

cprod_extraspecial [lemma, in maximal]

cprod_normal2 [lemma, in gproduct]

cprod_modl [lemma, in gproduct]

cprod_exponent [lemma, in abelian]

cprod_by_uniq [lemma, in center]

cprod_by [definition, in center]

cprod0g [lemma, in gproduct]

cprod1g [lemma, in gproduct]

critical [definition, in maximal]

critical_class2 [lemma, in maximal]

critical_p_stab_Aut [lemma, in maximal]

critical_extraspecial [lemma, in maximal]

curry_imset2X [lemma, in finset]

curry_imset2r [lemma, in finset]

curry_imset2l [lemma, in finset]

cycle [definition, in path]

cycle [definition, in fingroup]

CycleArc [section, in path]

CycleArc.T [variable, in path]

cycleJ [lemma, in fingroup]

cyclem [definition, in cyclic]

cycleM [lemma, in cyclic]

cyclemM [lemma, in cyclic]

cycleMsub [lemma, in cyclic]

cyclem_morphism [definition, in cyclic]

cycleP [lemma, in fingroup]

cyclePmin [lemma, in fingroup]

Cycles [section, in fingroup]

CycleSubGroup [section, in cyclic]

CycleSubGroup.gT [variable, in cyclic]

Cycles.gT [variable, in fingroup]

cycleV [lemma, in fingroup]

cycleX [lemma, in fingroup]

cycle_orbit [lemma, in fingraph]

cycle_group [definition, in fingroup]

cycle_path [lemma, in path]

cycle_id [lemma, in fingroup]

cycle_abelian [lemma, in fingroup]

cycle_cyclic [lemma, in cyclic]

cycle_rotr [lemma, in path]

cycle_rot [lemma, in path]

cycle_next [lemma, in path]

cycle_abelem [lemma, in abelian]

cycle_prev [lemma, in path]

cycle_eq1 [lemma, in fingroup]

cycle_from_next [lemma, in path]

cycle_sub_group [lemma, in cyclic]

cycle_subG [lemma, in fingroup]

cycle_constt [lemma, in pgroup]

cycle_repr_structure [lemma, in mxrepresentation]

cycle_generator [lemma, in cyclic]

cycle_subgroup_char [lemma, in cyclic]

cycle_traject [lemma, in fingroup]

cycle_from_prev [lemma, in path]

cycle1 [lemma, in fingroup]

cycle2g [lemma, in fingroup]

Cyclic [section, in cyclic]

cyclic [definition, in cyclic]

cyclic [library]

CyclicAutomorphism [section, in cyclic]

CyclicAutomorphism.CycleAutomorphism [section, in cyclic]

CyclicAutomorphism.CycleAutomorphism.a [variable, in cyclic]

CyclicAutomorphism.CycleAutomorphism.CycleMorphism [section, in cyclic]

CyclicAutomorphism.CycleAutomorphism.CycleMorphism.n [variable, in cyclic]

CyclicAutomorphism.CycleAutomorphism.ZpUnitMorphism [section, in cyclic]

CyclicAutomorphism.CycleAutomorphism.ZpUnitMorphism.u [variable, in cyclic]

CyclicAutomorphism.G [variable, in cyclic]

CyclicAutomorphism.gT [variable, in cyclic]

cyclicJ [lemma, in cyclic]

cyclicP [lemma, in cyclic]

CyclicProps [section, in cyclic]

CyclicProps.gT [variable, in cyclic]

cyclicS [lemma, in cyclic]

cyclic_mx_id [lemma, in mxrepresentation]

cyclic_mx_sub [lemma, in mxrepresentation]

cyclic_mxP [lemma, in mxrepresentation]

cyclic_mx_eq0 [lemma, in mxrepresentation]

cyclic_pgroup_quo_der1_cyclic [lemma, in sylow]

cyclic_center_factor_abelian [lemma, in center]

cyclic_SCN [lemma, in extremal]

cyclic_factor_abelian [lemma, in center]

cyclic_abelian [lemma, in cyclic]

cyclic_pgroup_dprod_trivg [lemma, in abelian]

cyclic_pgroup_Aut_structure [lemma, in extremal]

cyclic_abelem_prime [lemma, in abelian]

cyclic_small [lemma, in cyclic]

cyclic_metacyclic [lemma, in cyclic]

cyclic_mx [definition, in mxrepresentation]

cyclic_mx_module [lemma, in mxrepresentation]

Cyclic.gT [variable, in cyclic]

Cyclic.Zpm [section, in cyclic]

Cyclic.Zpm.a [variable, in cyclic]

cyclic1 [lemma, in cyclic]

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) |