| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +
C
+c [abbreviation, in mathcomp.character.character]+C [abbreviation, in mathcomp.solvable.center]
+cancel_index_extremal_groups [lemma, in mathcomp.solvable.extremal]
+CanChoiceMixin [definition, in mathcomp.ssreflect.choice]
+CanCountMixin [definition, in mathcomp.ssreflect.choice]
+CanEqMixin [definition, in mathcomp.ssreflect.eqtype]
+CanFinMixin [definition, in mathcomp.ssreflect.fintype]
+canF_invF [lemma, in mathcomp.ssreflect.fintype]
+canF_eq [lemma, in mathcomp.ssreflect.fintype]
+canF_RL [lemma, in mathcomp.ssreflect.fintype]
+canF_LR [lemma, in mathcomp.ssreflect.fintype]
+canF_sym [lemma, in mathcomp.ssreflect.fintype]
+Canonicals [section, in mathcomp.algebra.fraction]
+Canonicals.R [variable, in mathcomp.algebra.fraction]
+can_in_eq [lemma, in mathcomp.ssreflect.eqtype]
+can_eq [lemma, in mathcomp.ssreflect.eqtype]
+can_imset_pre [lemma, in mathcomp.ssreflect.finset]
+can2_mem_pmap [lemma, in mathcomp.ssreflect.seq]
+can2_eq [lemma, in mathcomp.ssreflect.eqtype]
+can2_imset_pre [lemma, in mathcomp.ssreflect.finset]
+can2_in_imset_pre [lemma, in mathcomp.ssreflect.finset]
+capfv [lemma, in mathcomp.algebra.vector]
+capmx [definition, in mathcomp.algebra.mxalgebra]
+capmxA [lemma, in mathcomp.algebra.mxalgebra]
+capmxC [lemma, in mathcomp.algebra.mxalgebra]
+capmxE [lemma, in mathcomp.algebra.mxalgebra]
+capmxMr [lemma, in mathcomp.algebra.mxalgebra]
+capmxS [lemma, in mathcomp.algebra.mxalgebra]
+capmxSl [lemma, in mathcomp.algebra.mxalgebra]
+capmxSr [lemma, in mathcomp.algebra.mxalgebra]
+capmxT [lemma, in mathcomp.algebra.mxalgebra]
+capmx_subSocle [lemma, in mathcomp.character.mxrepresentation]
+capmx_module [lemma, in mathcomp.character.mxrepresentation]
+capmx_diff [lemma, in mathcomp.algebra.mxalgebra]
+capmx_compl [lemma, in mathcomp.algebra.mxalgebra]
+capmx_idPl [lemma, in mathcomp.algebra.mxalgebra]
+capmx_idPr [lemma, in mathcomp.algebra.mxalgebra]
+capmx_key [lemma, in mathcomp.algebra.mxalgebra]
+capmx_def [definition, in mathcomp.algebra.mxalgebra]
+capmx_gen [definition, in mathcomp.algebra.mxalgebra]
+capmx0 [lemma, in mathcomp.algebra.mxalgebra]
+capmx1 [lemma, in mathcomp.algebra.mxalgebra]
+capTmx [lemma, in mathcomp.algebra.mxalgebra]
+capV [abbreviation, in mathcomp.algebra.vector]
+capv [definition, in mathcomp.algebra.vector]
+capvA [lemma, in mathcomp.algebra.vector]
+capvC [lemma, in mathcomp.algebra.vector]
+capvf [lemma, in mathcomp.algebra.vector]
+capvS [lemma, in mathcomp.algebra.vector]
+capvSl [lemma, in mathcomp.algebra.vector]
+capvSr [lemma, in mathcomp.algebra.vector]
+capvv [lemma, in mathcomp.algebra.vector]
+capv_diff [lemma, in mathcomp.algebra.vector]
+capv_compl [lemma, in mathcomp.algebra.vector]
+capv_idPr [lemma, in mathcomp.algebra.vector]
+capv_idPl [lemma, in mathcomp.algebra.vector]
+capv0 [lemma, in mathcomp.algebra.vector]
+cap_cfcenter_irr [lemma, in mathcomp.character.character]
+cap_cfker_lin_irr [lemma, in mathcomp.character.character]
+cap_cfker_normal [lemma, in mathcomp.character.character]
+cap_eqmx [lemma, in mathcomp.algebra.mxalgebra]
+cap0mx [lemma, in mathcomp.algebra.mxalgebra]
+cap0v [lemma, in mathcomp.algebra.vector]
+cap1mx [lemma, in mathcomp.algebra.mxalgebra]
+cardC [lemma, in mathcomp.ssreflect.fintype]
+CardCosetpre [section, in mathcomp.fingroup.quotient]
+CardCosetpre.G [variable, in mathcomp.fingroup.quotient]
+CardCosetpre.gT [variable, in mathcomp.fingroup.quotient]
+CardCosetpre.H [variable, in mathcomp.fingroup.quotient]
+CardCosetpre.K [variable, in mathcomp.fingroup.quotient]
+CardCosetpre.L [variable, in mathcomp.fingroup.quotient]
+CardCosetpre.M [variable, in mathcomp.fingroup.quotient]
+cardC1 [lemma, in mathcomp.ssreflect.fintype]
+CardDef [module, in mathcomp.ssreflect.fintype]
+CardDefSig [module, in mathcomp.ssreflect.fintype]
+CardDefSig.card [axiom, in mathcomp.ssreflect.fintype]
+CardDefSig.cardEdef [axiom, in mathcomp.ssreflect.fintype]
+CardDef.card [definition, in mathcomp.ssreflect.fintype]
+CardDef.cardEdef [definition, in mathcomp.ssreflect.fintype]
+cardD1 [lemma, in mathcomp.ssreflect.fintype]
+cardD1x [lemma, in mathcomp.ssreflect.bigop]
+cardE [lemma, in mathcomp.ssreflect.fintype]
+CardFunImage [section, in mathcomp.ssreflect.fintype]
+CardFunImage [section, in mathcomp.ssreflect.finset]
+CardFunImage.aT [variable, in mathcomp.ssreflect.finset]
+CardFunImage.aT2 [variable, in mathcomp.ssreflect.finset]
+CardFunImage.card_range [variable, in mathcomp.ssreflect.fintype]
+CardFunImage.D [variable, in mathcomp.ssreflect.finset]
+CardFunImage.D2 [variable, in mathcomp.ssreflect.finset]
+CardFunImage.f [variable, in mathcomp.ssreflect.fintype]
+CardFunImage.f [variable, in mathcomp.ssreflect.finset]
+CardFunImage.f2 [variable, in mathcomp.ssreflect.finset]
+CardFunImage.g [variable, in mathcomp.ssreflect.finset]
+CardFunImage.injf [variable, in mathcomp.ssreflect.fintype]
+CardFunImage.rT [variable, in mathcomp.ssreflect.finset]
+CardFunImage.T [variable, in mathcomp.ssreflect.fintype]
+CardFunImage.T' [variable, in mathcomp.ssreflect.fintype]
+CardGL [section, in mathcomp.algebra.mxalgebra]
+CardGL.F [variable, in mathcomp.algebra.mxalgebra]
+cardG_gt1 [lemma, in mathcomp.fingroup.fingroup]
+cardG_gt0_reduced [definition, in mathcomp.fingroup.fingroup]
+cardG_gt0 [lemma, in mathcomp.fingroup.fingroup]
+cardID [lemma, in mathcomp.ssreflect.fintype]
+cardIg_divn [lemma, in mathcomp.fingroup.fingroup]
+cardJg [lemma, in mathcomp.fingroup.fingroup]
+cardMg_TI [lemma, in mathcomp.fingroup.fingroup]
+cardMg_divn [lemma, in mathcomp.fingroup.fingroup]
+CardMorphism [section, in mathcomp.fingroup.quotient]
+CardMorphism.aT [variable, in mathcomp.fingroup.quotient]
+CardMorphism.D [variable, in mathcomp.fingroup.quotient]
+CardMorphism.f [variable, in mathcomp.fingroup.quotient]
+CardMorphism.rT [variable, in mathcomp.fingroup.quotient]
+cardsC [lemma, in mathcomp.ssreflect.finset]
+cardsCs [lemma, in mathcomp.ssreflect.finset]
+cardsC1 [lemma, in mathcomp.ssreflect.finset]
+cardsD [lemma, in mathcomp.ssreflect.finset]
+cardsDS [lemma, in mathcomp.ssreflect.finset]
+cardsD1 [lemma, in mathcomp.ssreflect.finset]
+cardsE [lemma, in mathcomp.ssreflect.finset]
+cardSg [lemma, in mathcomp.fingroup.fingroup]
+cardSg_cyclic [lemma, in mathcomp.solvable.cyclic]
+cardsI [lemma, in mathcomp.ssreflect.finset]
+cardsID [lemma, in mathcomp.ssreflect.finset]
+CardSig [section, in mathcomp.ssreflect.fintype]
+CardSig.P [variable, in mathcomp.ssreflect.fintype]
+CardSig.T [variable, in mathcomp.ssreflect.fintype]
+cardsT [lemma, in mathcomp.ssreflect.finset]
+cardsU [lemma, in mathcomp.ssreflect.finset]
+cardsUI [lemma, in mathcomp.ssreflect.finset]
+cardsU1 [lemma, in mathcomp.ssreflect.finset]
+cardsX [lemma, in mathcomp.ssreflect.finset]
+cards_draws [lemma, in mathcomp.ssreflect.binomial]
+cards_eq0 [lemma, in mathcomp.ssreflect.finset]
+cards0 [lemma, in mathcomp.ssreflect.finset]
+cards0_eq [lemma, in mathcomp.ssreflect.finset]
+cards1 [lemma, in mathcomp.ssreflect.finset]
+cards1P [lemma, in mathcomp.ssreflect.finset]
+cards2 [lemma, in mathcomp.ssreflect.finset]
+cardT [lemma, in mathcomp.ssreflect.fintype]
+cardUI [lemma, in mathcomp.ssreflect.fintype]
+cardU1 [lemma, in mathcomp.ssreflect.fintype]
+CardVspace [section, in mathcomp.field.finfield]
+CardVspace.aT [variable, in mathcomp.field.finfield]
+CardVspace.caT [variable, in mathcomp.field.finfield]
+CardVspace.F [variable, in mathcomp.field.finfield]
+CardVspace.T [variable, in mathcomp.field.finfield]
+CardVspace.Vector [section, in mathcomp.field.finfield]
+CardVspace.Vector.cvT [variable, in mathcomp.field.finfield]
+CardVspace.Vector.vT [variable, in mathcomp.field.finfield]
+cardX [lemma, in mathcomp.ssreflect.fintype]
+card_Alt [lemma, in mathcomp.solvable.alt]
+card_Sym [lemma, in mathcomp.solvable.alt]
+card_Hall [lemma, in mathcomp.solvable.pgroup]
+card_pgroup [lemma, in mathcomp.solvable.pgroup]
+card_cosetpre [lemma, in mathcomp.fingroup.quotient]
+card_homg [lemma, in mathcomp.fingroup.quotient]
+card_morphpre [lemma, in mathcomp.fingroup.quotient]
+card_morphim [lemma, in mathcomp.fingroup.quotient]
+card_quotient [lemma, in mathcomp.fingroup.quotient]
+card_quotient_subnorm [lemma, in mathcomp.fingroup.quotient]
+card_ord_partitions [lemma, in mathcomp.ssreflect.binomial]
+card_partial_ord_partitions [lemma, in mathcomp.ssreflect.binomial]
+card_sorted_tuples [lemma, in mathcomp.ssreflect.binomial]
+card_ltn_sorted_tuples [lemma, in mathcomp.ssreflect.binomial]
+card_draws [lemma, in mathcomp.ssreflect.binomial]
+card_inj_ffuns [lemma, in mathcomp.ssreflect.binomial]
+card_inj_ffuns_on [lemma, in mathcomp.ssreflect.binomial]
+card_uniq_tuples [lemma, in mathcomp.ssreflect.binomial]
+card_primeChar [lemma, in mathcomp.field.finfield]
+card_vspace1 [lemma, in mathcomp.field.finfield]
+card_vspacef [lemma, in mathcomp.field.finfield]
+card_vspace [lemma, in mathcomp.field.finfield]
+card_finCharP [lemma, in mathcomp.field.finfield]
+card_finField_unit [lemma, in mathcomp.field.finfield]
+card_support_normedTI [lemma, in mathcomp.solvable.frobenius]
+card_uniq_tuple [lemma, in mathcomp.solvable.primitive_action]
+card_perm [lemma, in mathcomp.fingroup.perm]
+card_linear_irr [lemma, in mathcomp.character.mxrepresentation]
+card_irr [lemma, in mathcomp.character.mxrepresentation]
+card_isog8_extraspecial [lemma, in mathcomp.solvable.extraspecial]
+card_DnQ [lemma, in mathcomp.solvable.extraspecial]
+card_pX1p2n [lemma, in mathcomp.solvable.extraspecial]
+card_pX1p2 [lemma, in mathcomp.solvable.extraspecial]
+card_tuple [lemma, in mathcomp.ssreflect.tuple]
+card_matrix [lemma, in mathcomp.algebra.matrix]
+card_subcent1_coset [lemma, in mathcomp.character.character]
+card_lin_irr [lemma, in mathcomp.character.character]
+card_afix_irr_classes [lemma, in mathcomp.character.character]
+card_Iirr_cyclic [lemma, in mathcomp.character.character]
+card_Iirr_abelian [lemma, in mathcomp.character.character]
+card_quaternion [lemma, in mathcomp.solvable.extremal]
+card_semidihedral [lemma, in mathcomp.solvable.extremal]
+card_2dihedral [lemma, in mathcomp.solvable.extremal]
+card_dihedral [lemma, in mathcomp.solvable.extremal]
+card_ext_dihedral [lemma, in mathcomp.solvable.extremal]
+card_modular_group [lemma, in mathcomp.solvable.extremal]
+card_cfclass_Iirr [lemma, in mathcomp.character.inertia]
+card_homocyclic [lemma, in mathcomp.solvable.abelian]
+card_p1Elem_p2Elem [lemma, in mathcomp.solvable.abelian]
+card_p1Elem_pnElem [lemma, in mathcomp.solvable.abelian]
+card_p1Elem [lemma, in mathcomp.solvable.abelian]
+card_pnElem [lemma, in mathcomp.solvable.abelian]
+card_extraspecial [lemma, in mathcomp.solvable.maximal]
+card_subcent_extraspecial [lemma, in mathcomp.solvable.maximal]
+card_p3group_extraspecial [lemma, in mathcomp.solvable.maximal]
+card_center_extraspecial [lemma, in mathcomp.solvable.maximal]
+card_sum [lemma, in mathcomp.ssreflect.fintype]
+card_tagged [lemma, in mathcomp.ssreflect.fintype]
+card_prod [lemma, in mathcomp.ssreflect.fintype]
+card_ord [lemma, in mathcomp.ssreflect.fintype]
+card_seq_sub [lemma, in mathcomp.ssreflect.fintype]
+card_sig [lemma, in mathcomp.ssreflect.fintype]
+card_sub [lemma, in mathcomp.ssreflect.fintype]
+card_option [lemma, in mathcomp.ssreflect.fintype]
+card_bool [lemma, in mathcomp.ssreflect.fintype]
+card_unit [lemma, in mathcomp.ssreflect.fintype]
+card_preim [lemma, in mathcomp.ssreflect.fintype]
+card_codom [lemma, in mathcomp.ssreflect.fintype]
+card_image [lemma, in mathcomp.ssreflect.fintype]
+card_in_image [lemma, in mathcomp.ssreflect.fintype]
+card_gt0P [lemma, in mathcomp.ssreflect.fintype]
+card_uniqP [lemma, in mathcomp.ssreflect.fintype]
+card_size [lemma, in mathcomp.ssreflect.fintype]
+card_def [abbreviation, in mathcomp.ssreflect.fintype]
+card_type [abbreviation, in mathcomp.ssreflect.fintype]
+card_classes_abelian [lemma, in mathcomp.fingroup.action]
+card_conjugates [lemma, in mathcomp.fingroup.action]
+card_orbit_stab [lemma, in mathcomp.fingroup.action]
+card_orbit [lemma, in mathcomp.fingroup.action]
+card_orbit_in_stab [lemma, in mathcomp.fingroup.action]
+card_orbit_in [lemma, in mathcomp.fingroup.action]
+card_orbit1 [lemma, in mathcomp.fingroup.action]
+card_setact [lemma, in mathcomp.fingroup.action]
+card_ffun [lemma, in mathcomp.ssreflect.finfun]
+card_ffun_on [lemma, in mathcomp.ssreflect.finfun]
+card_pffun_on [lemma, in mathcomp.ssreflect.finfun]
+card_family [lemma, in mathcomp.ssreflect.finfun]
+card_pfamily [lemma, in mathcomp.ssreflect.finfun]
+card_rVabelem [lemma, in mathcomp.character.mxabelem]
+card_abelem_rV [lemma, in mathcomp.character.mxabelem]
+card_rowg [lemma, in mathcomp.character.mxabelem]
+card_isog [lemma, in mathcomp.fingroup.morphism]
+card_injm [lemma, in mathcomp.fingroup.morphism]
+card_im_injm [lemma, in mathcomp.fingroup.morphism]
+card_lcosets [lemma, in mathcomp.fingroup.fingroup]
+card_le1_trivg [lemma, in mathcomp.fingroup.fingroup]
+card_rcoset [lemma, in mathcomp.fingroup.fingroup]
+card_lcoset [lemma, in mathcomp.fingroup.fingroup]
+card_invg [lemma, in mathcomp.fingroup.fingroup]
+card_mem_repr [lemma, in mathcomp.fingroup.fingroup]
+card_Fp [lemma, in mathcomp.algebra.zmodp]
+card_units_Zp [lemma, in mathcomp.algebra.zmodp]
+card_Zp [lemma, in mathcomp.algebra.zmodp]
+card_Aut_cyclic [lemma, in mathcomp.solvable.cyclic]
+card_Aut_cycle [lemma, in mathcomp.solvable.cyclic]
+card_GL_2 [lemma, in mathcomp.algebra.mxalgebra]
+card_GL_1 [lemma, in mathcomp.algebra.mxalgebra]
+card_GL [lemma, in mathcomp.algebra.mxalgebra]
+card_n3s [lemma, in mathcomp.solvable.burnside_app]
+card_n2_3 [lemma, in mathcomp.solvable.burnside_app]
+card_n3_3 [lemma, in mathcomp.solvable.burnside_app]
+card_n4 [lemma, in mathcomp.solvable.burnside_app]
+card_Fid3 [lemma, in mathcomp.solvable.burnside_app]
+card_n3 [lemma, in mathcomp.solvable.burnside_app]
+card_n [lemma, in mathcomp.solvable.burnside_app]
+card_n2 [lemma, in mathcomp.solvable.burnside_app]
+card_Fid [lemma, in mathcomp.solvable.burnside_app]
+card_rot [lemma, in mathcomp.solvable.burnside_app]
+card_iso2 [lemma, in mathcomp.solvable.burnside_app]
+card_transversal [lemma, in mathcomp.ssreflect.finset]
+card_uniform_partition [lemma, in mathcomp.ssreflect.finset]
+card_partition [lemma, in mathcomp.ssreflect.finset]
+card_powerset [lemma, in mathcomp.ssreflect.finset]
+card_preimset [lemma, in mathcomp.ssreflect.finset]
+card_imset [lemma, in mathcomp.ssreflect.finset]
+card_in_imset [lemma, in mathcomp.ssreflect.finset]
+card_gt0 [lemma, in mathcomp.ssreflect.finset]
+card_p2group_abelian [lemma, in mathcomp.solvable.sylow]
+card_Syl_mod [lemma, in mathcomp.solvable.sylow]
+card_Syl_dvd [lemma, in mathcomp.solvable.sylow]
+card_Syl [lemma, in mathcomp.solvable.sylow]
+card0 [lemma, in mathcomp.ssreflect.fintype]
+card0_eq [lemma, in mathcomp.ssreflect.fintype]
+card1 [lemma, in mathcomp.ssreflect.fintype]
+card1_trivg [lemma, in mathcomp.fingroup.fingroup]
+card2 [lemma, in mathcomp.ssreflect.fintype]
+CartesianProd [section, in mathcomp.ssreflect.finset]
+CartesianProd.A1 [variable, in mathcomp.ssreflect.finset]
+CartesianProd.A2 [variable, in mathcomp.ssreflect.finset]
+CartesianProd.fT1 [variable, in mathcomp.ssreflect.finset]
+CartesianProd.fT2 [variable, in mathcomp.ssreflect.finset]
+castmx [definition, in mathcomp.algebra.matrix]
+castmxE [lemma, in mathcomp.algebra.matrix]
+castmxK [lemma, in mathcomp.algebra.matrix]
+castmxKV [lemma, in mathcomp.algebra.matrix]
+castmx_sym [lemma, in mathcomp.algebra.matrix]
+castmx_comp [lemma, in mathcomp.algebra.matrix]
+castmx_id [lemma, in mathcomp.algebra.matrix]
+castmx_const [lemma, in mathcomp.algebra.matrix]
+CastTuple [section, in mathcomp.ssreflect.tuple]
+CastTuple.T [variable, in mathcomp.ssreflect.tuple]
+cast_col_mx [lemma, in mathcomp.algebra.matrix]
+cast_row_mx [lemma, in mathcomp.algebra.matrix]
+cast_ord_inj [lemma, in mathcomp.ssreflect.fintype]
+cast_ordKV [lemma, in mathcomp.ssreflect.fintype]
+cast_ordK [lemma, in mathcomp.ssreflect.fintype]
+cast_ord_comp [lemma, in mathcomp.ssreflect.fintype]
+cast_ord_id [lemma, in mathcomp.ssreflect.fintype]
+cast_ord [definition, in mathcomp.ssreflect.fintype]
+cast_ord_proof [lemma, in mathcomp.ssreflect.fintype]
+cat [definition, in mathcomp.ssreflect.seq]
+catA [lemma, in mathcomp.ssreflect.seq]
+catCA_perm_subst [lemma, in mathcomp.ssreflect.seq]
+catCA_perm_ind [lemma, in mathcomp.ssreflect.seq]
+catl_free [lemma, in mathcomp.algebra.vector]
+catrev [definition, in mathcomp.ssreflect.seq]
+catrevE [lemma, in mathcomp.ssreflect.seq]
+catrev_catr [lemma, in mathcomp.ssreflect.seq]
+catrev_catl [lemma, in mathcomp.ssreflect.seq]
+catr_free [lemma, in mathcomp.algebra.vector]
+cats0 [lemma, in mathcomp.ssreflect.seq]
+cats1 [lemma, in mathcomp.ssreflect.seq]
+cat_path [lemma, in mathcomp.ssreflect.path]
+cat_basis [lemma, in mathcomp.algebra.vector]
+cat_free [lemma, in mathcomp.algebra.vector]
+cat_tupleP [lemma, in mathcomp.ssreflect.tuple]
+cat_subseq [lemma, in mathcomp.ssreflect.seq]
+cat_uniq [lemma, in mathcomp.ssreflect.seq]
+cat_take_drop [lemma, in mathcomp.ssreflect.seq]
+cat_rcons [lemma, in mathcomp.ssreflect.seq]
+cat_nseq [lemma, in mathcomp.ssreflect.seq]
+cat_cons [lemma, in mathcomp.ssreflect.seq]
+cat0s [lemma, in mathcomp.ssreflect.seq]
+cat1s [lemma, in mathcomp.ssreflect.seq]
+Cauchy [lemma, in mathcomp.solvable.pgroup]
+Cayley_Hamilton [lemma, in mathcomp.algebra.mxpoly]
+Cayley_isog [lemma, in mathcomp.fingroup.action]
+Cayley_isom [lemma, in mathcomp.fingroup.action]
+Cayley_repr [definition, in mathcomp.fingroup.action]
+Cchar [definition, in mathcomp.field.algC]
+centC [lemma, in mathcomp.fingroup.fingroup]
+Center [section, in mathcomp.character.character]
+Center [section, in mathcomp.solvable.center]
+center [definition, in mathcomp.solvable.center]
+center [library]
+centerC [lemma, in mathcomp.solvable.center]
+centerP [lemma, in mathcomp.solvable.center]
+centerv_sub [lemma, in mathcomp.field.falgebra]
+center_kquo_cyclic [lemma, in mathcomp.character.mxrepresentation]
+center_sub_Inertia [lemma, in mathcomp.character.inertia]
+center_aut_extraspecial [lemma, in mathcomp.solvable.maximal]
+center_special_abelem [lemma, in mathcomp.solvable.maximal]
+center_nil_eq1 [lemma, in mathcomp.solvable.nilpotent]
+center_ncprod [lemma, in mathcomp.solvable.center]
+center_ncprod0 [lemma, in mathcomp.solvable.center]
+center_bigdprod [lemma, in mathcomp.solvable.center]
+center_dprod [lemma, in mathcomp.solvable.center]
+center_bigcprod [lemma, in mathcomp.solvable.center]
+center_cprod [lemma, in mathcomp.solvable.center]
+center_prod [lemma, in mathcomp.solvable.center]
+center_class_formula [lemma, in mathcomp.solvable.center]
+center_idP [lemma, in mathcomp.solvable.center]
+center_char [lemma, in mathcomp.solvable.center]
+center_abelian [lemma, in mathcomp.solvable.center]
+center_normal [lemma, in mathcomp.solvable.center]
+center_sub [lemma, in mathcomp.solvable.center]
+center_vspace [definition, in mathcomp.field.falgebra]
+center_mxP [lemma, in mathcomp.algebra.mxalgebra]
+center_mx_sub [lemma, in mathcomp.algebra.mxalgebra]
+center_mx [definition, in mathcomp.algebra.mxalgebra]
+Center.G [variable, in mathcomp.character.character]
+Center.gT [variable, in mathcomp.character.character]
+Center.gT [variable, in mathcomp.solvable.center]
+Center.Injm [section, in mathcomp.solvable.center]
+Center.Injm.D [variable, in mathcomp.solvable.center]
+Center.Injm.f [variable, in mathcomp.solvable.center]
+Center.Injm.injf [variable, in mathcomp.solvable.center]
+Center.Injm.rT [variable, in mathcomp.solvable.center]
+center1 [lemma, in mathcomp.solvable.center]
+centgmx [definition, in mathcomp.character.mxrepresentation]
+centgmxP [lemma, in mathcomp.character.mxrepresentation]
+centgmx_map [lemma, in mathcomp.character.mxrepresentation]
+centgmx_hom [lemma, in mathcomp.character.mxrepresentation]
+centI [lemma, in mathcomp.fingroup.fingroup]
+centJ [lemma, in mathcomp.fingroup.fingroup]
+centM [lemma, in mathcomp.fingroup.fingroup]
+centP [lemma, in mathcomp.fingroup.fingroup]
+Central [section, in mathcomp.solvable.gseries]
+centralised [definition, in mathcomp.fingroup.fingroup]
+centraliser [definition, in mathcomp.fingroup.fingroup]
+centraliser_is_aspace [lemma, in mathcomp.field.falgebra]
+centraliser_vspace [definition, in mathcomp.field.falgebra]
+centraliser1_is_aspace [lemma, in mathcomp.field.falgebra]
+centraliser1_vspace [definition, in mathcomp.field.falgebra]
+centralises [definition, in mathcomp.fingroup.fingroup]
+centrals_nil [lemma, in mathcomp.solvable.nilpotent]
+central_product [definition, in mathcomp.fingroup.gproduct]
+central_central_factor [lemma, in mathcomp.solvable.gseries]
+central_factor_central [lemma, in mathcomp.solvable.gseries]
+central_factor [definition, in mathcomp.solvable.gseries]
+Central.G [variable, in mathcomp.solvable.gseries]
+Central.gT [variable, in mathcomp.solvable.gseries]
+centS [lemma, in mathcomp.fingroup.fingroup]
+centsC [lemma, in mathcomp.fingroup.fingroup]
+centsP [lemma, in mathcomp.fingroup.fingroup]
+centSS [lemma, in mathcomp.fingroup.fingroup]
+centsS [lemma, in mathcomp.fingroup.fingroup]
+cents_cycle [lemma, in mathcomp.fingroup.fingroup]
+cents_norm [lemma, in mathcomp.fingroup.fingroup]
+cents1 [lemma, in mathcomp.fingroup.fingroup]
+centU [lemma, in mathcomp.fingroup.fingroup]
+centvC [lemma, in mathcomp.field.falgebra]
+centvP [lemma, in mathcomp.field.falgebra]
+centvsP [lemma, in mathcomp.field.falgebra]
+centvX [lemma, in mathcomp.field.falgebra]
+centv_algid [lemma, in mathcomp.field.falgebra]
+centv1 [lemma, in mathcomp.field.falgebra]
+centY [lemma, in mathcomp.fingroup.fingroup]
+cent_semiregular [lemma, in mathcomp.solvable.frobenius]
+cent_semiprime [lemma, in mathcomp.solvable.frobenius]
+cent_mx_scalar_abs_irr [lemma, in mathcomp.character.mxrepresentation]
+cent_sub_Inertia [lemma, in mathcomp.character.inertia]
+cent_sub_inertia [lemma, in mathcomp.character.inertia]
+cent_classP [lemma, in mathcomp.fingroup.fingroup]
+cent_cycle [lemma, in mathcomp.fingroup.fingroup]
+cent_gen [lemma, in mathcomp.fingroup.fingroup]
+cent_normal [lemma, in mathcomp.fingroup.fingroup]
+cent_norm [lemma, in mathcomp.fingroup.fingroup]
+cent_joinEr [lemma, in mathcomp.fingroup.fingroup]
+cent_joinEl [lemma, in mathcomp.fingroup.fingroup]
+cent_sub [lemma, in mathcomp.fingroup.fingroup]
+cent_set1 [lemma, in mathcomp.fingroup.fingroup]
+cent_centerv [lemma, in mathcomp.field.falgebra]
+cent_mx_ring [lemma, in mathcomp.algebra.mxalgebra]
+cent_mx_ideal [lemma, in mathcomp.algebra.mxalgebra]
+cent_mxP [lemma, in mathcomp.algebra.mxalgebra]
+cent_rowP [lemma, in mathcomp.algebra.mxalgebra]
+cent_mx [definition, in mathcomp.algebra.mxalgebra]
+cent_mx_fun_is_linear [lemma, in mathcomp.algebra.mxalgebra]
+cent_mx_fun [definition, in mathcomp.algebra.mxalgebra]
+cent1C [lemma, in mathcomp.fingroup.fingroup]
+cent1E [lemma, in mathcomp.fingroup.fingroup]
+cent1id [lemma, in mathcomp.fingroup.fingroup]
+cent1J [lemma, in mathcomp.fingroup.fingroup]
+cent1P [lemma, in mathcomp.fingroup.fingroup]
+cent1T [lemma, in mathcomp.fingroup.fingroup]
+cent1vC [lemma, in mathcomp.field.falgebra]
+cent1vP [lemma, in mathcomp.field.falgebra]
+cent1vX [lemma, in mathcomp.field.falgebra]
+cent1v_id [lemma, in mathcomp.field.falgebra]
+cent1v1 [lemma, in mathcomp.field.falgebra]
+cent1_normedTI [lemma, in mathcomp.solvable.frobenius]
+cent1_extraspecial_maximal [lemma, in mathcomp.solvable.maximal]
+cent11T [lemma, in mathcomp.fingroup.fingroup]
+cfaithful [definition, in mathcomp.character.classfun]
+cfaithfulE [lemma, in mathcomp.character.classfun]
+cfaithful_reg [lemma, in mathcomp.character.character]
+cfaithful_quo [lemma, in mathcomp.character.classfun]
+cfAut [definition, in mathcomp.character.classfun]
+cfAutConjg [lemma, in mathcomp.character.inertia]
+cfAutDprod [lemma, in mathcomp.character.classfun]
+cfAutDprodl [lemma, in mathcomp.character.classfun]
+cfAutDprodr [lemma, in mathcomp.character.classfun]
+cfAutInd [lemma, in mathcomp.character.classfun]
+cfAutIsom [lemma, in mathcomp.character.classfun]
+cfAutK [lemma, in mathcomp.character.classfun]
+cfAutMod [lemma, in mathcomp.character.classfun]
+cfAutMorph [lemma, in mathcomp.character.classfun]
+cfAutQuo [lemma, in mathcomp.character.classfun]
+cfAutRes [lemma, in mathcomp.character.classfun]
+cfAutVK [lemma, in mathcomp.character.classfun]
+cfAutZ [lemma, in mathcomp.character.classfun]
+cfAutZ_Cint [lemma, in mathcomp.character.classfun]
+cfAutZ_Cnat [lemma, in mathcomp.character.classfun]
+cfAutZ_nat [lemma, in mathcomp.character.classfun]
+cfAut_vchar [lemma, in mathcomp.character.vcharacter]
+cfAut_zchar [lemma, in mathcomp.character.vcharacter]
+cfAut_irr [lemma, in mathcomp.character.character]
+cfAut_lin_char [lemma, in mathcomp.character.character]
+cfAut_irr1 [lemma, in mathcomp.character.character]
+cfAut_char1 [lemma, in mathcomp.character.character]
+cfAut_char [lemma, in mathcomp.character.character]
+cfAut_cfuni [lemma, in mathcomp.character.classfun]
+cfAut_on [lemma, in mathcomp.character.classfun]
+cfAut_eq1 [lemma, in mathcomp.character.classfun]
+cfAut_inj [lemma, in mathcomp.character.classfun]
+cfAut_closed [definition, in mathcomp.character.classfun]
+cfAut_scalable [lemma, in mathcomp.character.classfun]
+cfAut_cfun1 [lemma, in mathcomp.character.classfun]
+cfAut_is_rmorphism [lemma, in mathcomp.character.classfun]
+cfAut_cfun1i [lemma, in mathcomp.character.classfun]
+cfBigdprod [definition, in mathcomp.character.classfun]
+cfBigdprodE [lemma, in mathcomp.character.classfun]
+cfBigdprodEi [lemma, in mathcomp.character.classfun]
+cfBigdprodi [definition, in mathcomp.character.classfun]
+cfBigdprodiK [lemma, in mathcomp.character.classfun]
+cfBigdprodi_irr [lemma, in mathcomp.character.character]
+cfBigdprodi_lin_charE [lemma, in mathcomp.character.character]
+cfBigdprodi_lin_char [lemma, in mathcomp.character.character]
+cfBigdprodi_charE [lemma, in mathcomp.character.character]
+cfBigdprodi_char [lemma, in mathcomp.character.character]
+cfBigdprodi_iso [lemma, in mathcomp.character.classfun]
+cfBigdprodi_inj [lemma, in mathcomp.character.classfun]
+cfBigdprodi_eq1 [lemma, in mathcomp.character.classfun]
+cfBigdprodi_subproof [lemma, in mathcomp.character.classfun]
+cfBigdprodi1 [lemma, in mathcomp.character.classfun]
+cfBigdprodK [lemma, in mathcomp.character.classfun]
+cfBigdprodKabelian [lemma, in mathcomp.character.character]
+cfBigdprodKlin [lemma, in mathcomp.character.character]
+cfBigdprod_Res_lin [lemma, in mathcomp.character.character]
+cfBigdprod_eq1 [lemma, in mathcomp.character.character]
+cfBigdprod_irr [lemma, in mathcomp.character.character]
+cfBigdprod_lin_char [lemma, in mathcomp.character.character]
+cfBigdprod_char [lemma, in mathcomp.character.character]
+cfBigdprod1 [lemma, in mathcomp.character.classfun]
+cfCauchySchwarz [lemma, in mathcomp.character.classfun]
+cfCauchySchwarz_sqrt [lemma, in mathcomp.character.classfun]
+cfcenter [definition, in mathcomp.character.character]
+cfcenter_fful_irr [lemma, in mathcomp.character.character]
+cfcenter_eq_center [lemma, in mathcomp.character.character]
+cfcenter_subset_center [lemma, in mathcomp.character.character]
+cfcenter_cyclic [lemma, in mathcomp.character.character]
+cfcenter_Res [lemma, in mathcomp.character.character]
+cfcenter_normal [lemma, in mathcomp.character.character]
+cfcenter_sub [lemma, in mathcomp.character.character]
+cfcenter_group_set [lemma, in mathcomp.character.character]
+cfcenter_repr [lemma, in mathcomp.character.character]
+cfclass [definition, in mathcomp.character.inertia]
+cfclassInorm [lemma, in mathcomp.character.inertia]
+cfclassP [lemma, in mathcomp.character.inertia]
+cfclass_inertia [lemma, in mathcomp.character.inertia]
+cfclass_Ind [lemma, in mathcomp.character.inertia]
+cfclass_IirrE [lemma, in mathcomp.character.inertia]
+cfclass_Iirr [definition, in mathcomp.character.inertia]
+cfclass_invariant [lemma, in mathcomp.character.inertia]
+cfclass_uniq [lemma, in mathcomp.character.inertia]
+cfclass_sym [lemma, in mathcomp.character.inertia]
+cfclass_transr [lemma, in mathcomp.character.inertia]
+cfclass_refl [lemma, in mathcomp.character.inertia]
+cfclass1 [lemma, in mathcomp.character.inertia]
+cfConjCE [lemma, in mathcomp.character.classfun]
+cfConjCK [lemma, in mathcomp.character.classfun]
+cfConjC_vchar [definition, in mathcomp.character.vcharacter]
+cfConjC_irr [lemma, in mathcomp.character.character]
+cfConjC_lin_char [lemma, in mathcomp.character.character]
+cfConjC_irr1 [lemma, in mathcomp.character.character]
+cfConjC_char1 [lemma, in mathcomp.character.character]
+cfConjC_char [lemma, in mathcomp.character.character]
+cfconjC_eq1 [definition, in mathcomp.character.classfun]
+cfConjC_cfun1 [lemma, in mathcomp.character.classfun]
+cfConjC_closed [abbreviation, in mathcomp.character.classfun]
+cfConjC_subset [definition, in mathcomp.character.classfun]
+cfConjg [definition, in mathcomp.character.inertia]
+cfConjgBigdprod [lemma, in mathcomp.character.inertia]
+cfConjgBigdprodi [lemma, in mathcomp.character.inertia]
+cfConjgDprod [lemma, in mathcomp.character.inertia]
+cfConjgDprodl [lemma, in mathcomp.character.inertia]
+cfConjgDprodr [lemma, in mathcomp.character.inertia]
+cfConjgE [lemma, in mathcomp.character.inertia]
+cfConjgEin [lemma, in mathcomp.character.inertia]
+cfConjgEJ [lemma, in mathcomp.character.inertia]
+cfConjgEout [lemma, in mathcomp.character.inertia]
+cfConjgInd [lemma, in mathcomp.character.inertia]
+cfConjgInd_norm [lemma, in mathcomp.character.inertia]
+cfConjgIsom [lemma, in mathcomp.character.inertia]
+cfConjgJ1 [lemma, in mathcomp.character.inertia]
+cfConjgK [lemma, in mathcomp.character.inertia]
+cfConjgKV [lemma, in mathcomp.character.inertia]
+cfConjgM [lemma, in mathcomp.character.inertia]
+cfConjgMnorm [lemma, in mathcomp.character.inertia]
+cfConjgMod [lemma, in mathcomp.character.inertia]
+cfConjgMod_norm [lemma, in mathcomp.character.inertia]
+cfConjgMorph [lemma, in mathcomp.character.inertia]
+cfConjgQuo [lemma, in mathcomp.character.inertia]
+cfConjgQuo_norm [lemma, in mathcomp.character.inertia]
+cfConjgRes [lemma, in mathcomp.character.inertia]
+cfConjgRes_norm [lemma, in mathcomp.character.inertia]
+cfConjgSdprod [lemma, in mathcomp.character.inertia]
+cfConjg_irr [lemma, in mathcomp.character.inertia]
+cfConjg_lin_char [lemma, in mathcomp.character.inertia]
+cfConjg_char [lemma, in mathcomp.character.inertia]
+cfConjg_iso [lemma, in mathcomp.character.inertia]
+cfConjg_eqE [lemma, in mathcomp.character.inertia]
+cfConjg_eq1 [lemma, in mathcomp.character.inertia]
+cfConjg_is_multiplicative [lemma, in mathcomp.character.inertia]
+cfConjg_cfun1 [lemma, in mathcomp.character.inertia]
+cfConjg_cfuni [lemma, in mathcomp.character.inertia]
+cfConjg_cfuniJ [lemma, in mathcomp.character.inertia]
+cfConjg_is_linear [lemma, in mathcomp.character.inertia]
+cfConjg_id [lemma, in mathcomp.character.inertia]
+cfConjg_subproof [lemma, in mathcomp.character.inertia]
+cfConjg1 [lemma, in mathcomp.character.inertia]
+cfDet [definition, in mathcomp.character.character]
+cfDetConjg [lemma, in mathcomp.character.inertia]
+cfDetD [lemma, in mathcomp.character.character]
+cfDetIsom [lemma, in mathcomp.character.character]
+cfDetMn [lemma, in mathcomp.character.character]
+cfDetMorph [lemma, in mathcomp.character.character]
+CfDetOps [section, in mathcomp.character.character]
+cfDetRepr [lemma, in mathcomp.character.character]
+cfDetRes [lemma, in mathcomp.character.character]
+cfDet_mul_lin [lemma, in mathcomp.character.character]
+cfDet_order_dvdG [definition, in mathcomp.character.character]
+cfDet_order_lin [definition, in mathcomp.character.character]
+cfDet_order [definition, in mathcomp.character.character]
+cfDet_id [lemma, in mathcomp.character.character]
+cfDet_lin_char [lemma, in mathcomp.character.character]
+cfDet0 [lemma, in mathcomp.character.character]
+cfdot [definition, in mathcomp.character.classfun]
+cfdotBl [lemma, in mathcomp.character.classfun]
+cfdotBr [lemma, in mathcomp.character.classfun]
+cfdotC [lemma, in mathcomp.character.classfun]
+cfdotC_char [lemma, in mathcomp.character.character]
+cfdotDl [lemma, in mathcomp.character.classfun]
+cfdotDr [lemma, in mathcomp.character.classfun]
+cfdotE [lemma, in mathcomp.character.classfun]
+cfdotEl [lemma, in mathcomp.character.classfun]
+cfdotElr [lemma, in mathcomp.character.classfun]
+cfdotEr [lemma, in mathcomp.character.classfun]
+cfdotMnl [lemma, in mathcomp.character.classfun]
+cfdotMnr [lemma, in mathcomp.character.classfun]
+cfdotNl [lemma, in mathcomp.character.classfun]
+cfdotNr [lemma, in mathcomp.character.classfun]
+cfdotr [abbreviation, in mathcomp.character.classfun]
+cfdotrE [lemma, in mathcomp.character.classfun]
+cfdotr_is_linear [lemma, in mathcomp.character.classfun]
+cfdotr_head [definition, in mathcomp.character.classfun]
+cfdotZl [lemma, in mathcomp.character.classfun]
+cfdotZr [lemma, in mathcomp.character.classfun]
+cfdot_add_dirr_eq1 [lemma, in mathcomp.character.vcharacter]
+cfdot_dirr_eq1 [lemma, in mathcomp.character.vcharacter]
+cfdot_sum_dchi [lemma, in mathcomp.character.vcharacter]
+cfdot_todirrE [lemma, in mathcomp.character.vcharacter]
+cfdot_dchi [lemma, in mathcomp.character.vcharacter]
+cfdot_dirr [lemma, in mathcomp.character.vcharacter]
+cfdot_aut_vchar [lemma, in mathcomp.character.vcharacter]
+cfdot_sum_orthonormal [lemma, in mathcomp.character.vcharacter]
+cfdot_sum_orthogonal [lemma, in mathcomp.character.vcharacter]
+cfdot_vchar_r [lemma, in mathcomp.character.vcharacter]
+cfdot_aut_irr [lemma, in mathcomp.character.character]
+cfdot_aut_char [lemma, in mathcomp.character.character]
+cfdot_dprod_irr [lemma, in mathcomp.character.character]
+cfdot_Res_ge_constt [lemma, in mathcomp.character.character]
+cfdot_char_r [lemma, in mathcomp.character.character]
+cfdot_sum_irr [lemma, in mathcomp.character.character]
+cfdot_irr [lemma, in mathcomp.character.character]
+cfdot_irr_conjg [lemma, in mathcomp.character.inertia]
+cfdot_Res_conjg [lemma, in mathcomp.character.inertia]
+cfdot_Res_l [lemma, in mathcomp.character.classfun]
+cfdot_Res_r [definition, in mathcomp.character.classfun]
+cfdot_bigdprod [lemma, in mathcomp.character.classfun]
+cfdot_dprod [lemma, in mathcomp.character.classfun]
+cfdot_real_conjC [lemma, in mathcomp.character.classfun]
+cfdot_conjCr [lemma, in mathcomp.character.classfun]
+cfdot_conjCl [lemma, in mathcomp.character.classfun]
+cfdot_conjC [lemma, in mathcomp.character.classfun]
+cfdot_cfAut [lemma, in mathcomp.character.classfun]
+cfdot_sumr [lemma, in mathcomp.character.classfun]
+cfdot_suml [lemma, in mathcomp.character.classfun]
+cfdot_cfuni [lemma, in mathcomp.character.classfun]
+cfdot_complement [lemma, in mathcomp.character.classfun]
+cfdot0l [lemma, in mathcomp.character.classfun]
+cfdot0r [lemma, in mathcomp.character.classfun]
+cfDprod [definition, in mathcomp.character.classfun]
+cfDprodC [lemma, in mathcomp.character.classfun]
+cfDprodE [lemma, in mathcomp.character.classfun]
+cfDprodEl [lemma, in mathcomp.character.classfun]
+cfDprodEr [lemma, in mathcomp.character.classfun]
+cfDprodKl [lemma, in mathcomp.character.classfun]
+cfDprodKl_abelian [lemma, in mathcomp.character.character]
+cfDprodKr [lemma, in mathcomp.character.classfun]
+cfDprodKr_abelian [lemma, in mathcomp.character.character]
+cfDprodl [definition, in mathcomp.character.classfun]
+cfDprodlK [lemma, in mathcomp.character.classfun]
+cfDprodl_irr [lemma, in mathcomp.character.character]
+cfDprodl_lin_char [lemma, in mathcomp.character.character]
+cfDprodl_char [lemma, in mathcomp.character.character]
+cfDprodl_iso [lemma, in mathcomp.character.classfun]
+cfDprodl_eq1 [lemma, in mathcomp.character.classfun]
+cfDprodl1 [lemma, in mathcomp.character.classfun]
+cfDprodr [definition, in mathcomp.character.classfun]
+cfDprodrK [lemma, in mathcomp.character.classfun]
+cfDprodr_irr [lemma, in mathcomp.character.character]
+cfDprodr_lin_char [lemma, in mathcomp.character.character]
+cfDprodr_char [lemma, in mathcomp.character.character]
+cfDprodr_iso [lemma, in mathcomp.character.classfun]
+cfDprodr_eq1 [lemma, in mathcomp.character.classfun]
+cfDprodr1 [lemma, in mathcomp.character.classfun]
+cfDprod_irr [lemma, in mathcomp.character.character]
+cfDprod_lin_char [lemma, in mathcomp.character.character]
+cfDprod_eq1 [lemma, in mathcomp.character.character]
+cfDprod_char [lemma, in mathcomp.character.character]
+cfDprod_Resr [lemma, in mathcomp.character.classfun]
+cfDprod_Resl [lemma, in mathcomp.character.classfun]
+cfDprod_split [lemma, in mathcomp.character.classfun]
+cfDprod_cfun1 [lemma, in mathcomp.character.classfun]
+cfDprod_cfun1l [lemma, in mathcomp.character.classfun]
+cfDprod_cfun1r [lemma, in mathcomp.character.classfun]
+cfDprod1 [lemma, in mathcomp.character.classfun]
+cfExp_prime_transitive [lemma, in mathcomp.character.character]
+cfIirr [definition, in mathcomp.character.character]
+cfIirrE [lemma, in mathcomp.character.character]
+cfIirrPE [lemma, in mathcomp.character.character]
+cfInd [definition, in mathcomp.character.classfun]
+cfIndE [lemma, in mathcomp.character.classfun]
+cfIndEout [lemma, in mathcomp.character.classfun]
+cfIndEsdprod [lemma, in mathcomp.character.classfun]
+cfIndInd [lemma, in mathcomp.character.classfun]
+cfIndIsom [lemma, in mathcomp.character.classfun]
+cfIndM [lemma, in mathcomp.character.classfun]
+cfIndMorph [lemma, in mathcomp.character.classfun]
+cfInd_vchar [lemma, in mathcomp.character.vcharacter]
+cfInd_eq0 [lemma, in mathcomp.character.character]
+cfInd_char [lemma, in mathcomp.character.character]
+cfInd_cfun1 [lemma, in mathcomp.character.classfun]
+cfInd_normal [lemma, in mathcomp.character.classfun]
+cfInd_id [lemma, in mathcomp.character.classfun]
+cfInd_on [lemma, in mathcomp.character.classfun]
+cfInd_is_linear [lemma, in mathcomp.character.classfun]
+cfInd_subproof [lemma, in mathcomp.character.classfun]
+cfInd1 [lemma, in mathcomp.character.classfun]
+cfIsom [definition, in mathcomp.character.classfun]
+cfIsomE [lemma, in mathcomp.character.classfun]
+cfIsomK [lemma, in mathcomp.character.classfun]
+cfIsomKV [lemma, in mathcomp.character.classfun]
+cfIsom_irr [lemma, in mathcomp.character.character]
+cfIsom_lin_char [lemma, in mathcomp.character.character]
+cfIsom_char [lemma, in mathcomp.character.character]
+cfIsom_iso [lemma, in mathcomp.character.classfun]
+cfIsom_eq1 [lemma, in mathcomp.character.classfun]
+cfIsom_inj [lemma, in mathcomp.character.classfun]
+cfIsom_cfun1 [lemma, in mathcomp.character.classfun]
+cfIsom_key [lemma, in mathcomp.character.classfun]
+cfIsom1 [lemma, in mathcomp.character.classfun]
+cfker [definition, in mathcomp.character.classfun]
+cfkerE [lemma, in mathcomp.character.character]
+cfkerEchar [lemma, in mathcomp.character.character]
+cfkerEirr [lemma, in mathcomp.character.character]
+cfkerMl [lemma, in mathcomp.character.classfun]
+cfkerMr [lemma, in mathcomp.character.classfun]
+cfker_Ind_irr [lemma, in mathcomp.character.character]
+cfker_Ind [lemma, in mathcomp.character.character]
+cfker_Res [lemma, in mathcomp.character.character]
+cfker_center_normal [lemma, in mathcomp.character.character]
+cfker_reg_quo [lemma, in mathcomp.character.character]
+cfker_constt [lemma, in mathcomp.character.character]
+cfker_irr0 [lemma, in mathcomp.character.character]
+cfker_nzcharE [lemma, in mathcomp.character.character]
+cfker_repr [lemma, in mathcomp.character.character]
+cfker_conjg [lemma, in mathcomp.character.inertia]
+cfker_conjC [definition, in mathcomp.character.classfun]
+cfker_aut [lemma, in mathcomp.character.classfun]
+cfker_dprod [lemma, in mathcomp.character.classfun]
+cfker_dprodr [lemma, in mathcomp.character.classfun]
+cfker_dprodl [lemma, in mathcomp.character.classfun]
+cfker_sdprod [lemma, in mathcomp.character.classfun]
+cfker_quo [lemma, in mathcomp.character.classfun]
+cfker_mod [lemma, in mathcomp.character.classfun]
+cfker_isom [lemma, in mathcomp.character.classfun]
+cfker_morph_im [lemma, in mathcomp.character.classfun]
+cfker_morph [lemma, in mathcomp.character.classfun]
+cfker_prod [lemma, in mathcomp.character.classfun]
+cfker_mul [lemma, in mathcomp.character.classfun]
+cfker_cfun1 [lemma, in mathcomp.character.classfun]
+cfker_opp [lemma, in mathcomp.character.classfun]
+cfker_scale_nz [lemma, in mathcomp.character.classfun]
+cfker_scale [lemma, in mathcomp.character.classfun]
+cfker_sum [lemma, in mathcomp.character.classfun]
+cfker_add [lemma, in mathcomp.character.classfun]
+cfker_cfun0 [lemma, in mathcomp.character.classfun]
+cfker_normal [lemma, in mathcomp.character.classfun]
+cfker_norm [lemma, in mathcomp.character.classfun]
+cfker_sub [lemma, in mathcomp.character.classfun]
+cfker_is_group [lemma, in mathcomp.character.classfun]
+cfker1 [lemma, in mathcomp.character.classfun]
+cfMod [definition, in mathcomp.character.classfun]
+cfModE [lemma, in mathcomp.character.classfun]
+cfModK [lemma, in mathcomp.character.classfun]
+cfMod_irr [lemma, in mathcomp.character.character]
+cfMod_lin_charE [lemma, in mathcomp.character.character]
+cfMod_charE [lemma, in mathcomp.character.character]
+cfMod_lin_char [lemma, in mathcomp.character.character]
+cfMod_char [lemma, in mathcomp.character.character]
+cfMod_iso [lemma, in mathcomp.character.classfun]
+cfMod_eq1 [lemma, in mathcomp.character.classfun]
+cfMod_cfun1 [lemma, in mathcomp.character.classfun]
+cfMod1 [lemma, in mathcomp.character.classfun]
+cfMorph [definition, in mathcomp.character.classfun]
+cfMorphE [lemma, in mathcomp.character.classfun]
+cfMorphEout [lemma, in mathcomp.character.classfun]
+cfMorph_irr [lemma, in mathcomp.character.character]
+cfMorph_lin_charE [lemma, in mathcomp.character.character]
+cfMorph_charE [lemma, in mathcomp.character.character]
+cfMorph_lin_char [lemma, in mathcomp.character.character]
+cfMorph_char [lemma, in mathcomp.character.character]
+cfMorph_iso [lemma, in mathcomp.character.classfun]
+cfMorph_eq1 [lemma, in mathcomp.character.classfun]
+cfMorph_inj [lemma, in mathcomp.character.classfun]
+cfMorph_is_multiplicative [lemma, in mathcomp.character.classfun]
+cfMorph_is_linear [lemma, in mathcomp.character.classfun]
+cfMorph_cfun1 [lemma, in mathcomp.character.classfun]
+cfMorph_subproof [lemma, in mathcomp.character.classfun]
+cfMorph1 [lemma, in mathcomp.character.classfun]
+cfnorm [abbreviation, in mathcomp.character.classfun]
+cfnormB [lemma, in mathcomp.character.classfun]
+cfnormBd [lemma, in mathcomp.character.classfun]
+cfnormD [lemma, in mathcomp.character.classfun]
+cfnormDd [lemma, in mathcomp.character.classfun]
+cfnormE [lemma, in mathcomp.character.classfun]
+cfnormN [lemma, in mathcomp.character.classfun]
+cfnormZ [lemma, in mathcomp.character.classfun]
+cfnorm_dchi [lemma, in mathcomp.character.vcharacter]
+cfnorm_orthonormal [lemma, in mathcomp.character.vcharacter]
+cfnorm_map_orthonormal [lemma, in mathcomp.character.vcharacter]
+cfnorm_sum_orthonormal [lemma, in mathcomp.character.vcharacter]
+cfnorm_orthogonal [lemma, in mathcomp.character.vcharacter]
+cfnorm_sum_orthogonal [lemma, in mathcomp.character.vcharacter]
+cfnorm_Res_lerif [lemma, in mathcomp.character.character]
+cfnorm_irr [lemma, in mathcomp.character.character]
+cfnorm_Ind_cfun1 [lemma, in mathcomp.character.classfun]
+cfnorm_quo [lemma, in mathcomp.character.classfun]
+cfnorm_conjC [lemma, in mathcomp.character.classfun]
+cfnorm_sign [lemma, in mathcomp.character.classfun]
+cfnorm_gt0 [lemma, in mathcomp.character.classfun]
+cfnorm_eq0 [lemma, in mathcomp.character.classfun]
+cfnorm_ge0 [lemma, in mathcomp.character.classfun]
+cfnorm_head [definition, in mathcomp.character.classfun]
+cfnorm1 [lemma, in mathcomp.character.classfun]
+cforder [definition, in mathcomp.character.classfun]
+cforder_lin_char_gt0 [lemma, in mathcomp.character.character]
+cforder_lin_char_dvdG [lemma, in mathcomp.character.character]
+cforder_lin_char [lemma, in mathcomp.character.character]
+cforder_irr_eq1 [lemma, in mathcomp.character.character]
+cforder_aut [lemma, in mathcomp.character.classfun]
+cforder_dprodr [lemma, in mathcomp.character.classfun]
+cforder_dprodl [lemma, in mathcomp.character.classfun]
+cforder_sdprod [lemma, in mathcomp.character.classfun]
+cforder_quo [lemma, in mathcomp.character.classfun]
+cforder_mod [lemma, in mathcomp.character.classfun]
+cforder_isom [lemma, in mathcomp.character.classfun]
+cforder_morph [lemma, in mathcomp.character.classfun]
+cforder_Res [lemma, in mathcomp.character.classfun]
+cforder_inj_rmorph [lemma, in mathcomp.character.classfun]
+cforder_rmorph [lemma, in mathcomp.character.classfun]
+cfproj_sum_orthonormal [lemma, in mathcomp.character.vcharacter]
+cfproj_sum_orthogonal [lemma, in mathcomp.character.vcharacter]
+cfQuo [definition, in mathcomp.character.classfun]
+cfQuoE [lemma, in mathcomp.character.classfun]
+cfQuoEker [lemma, in mathcomp.character.classfun]
+cfQuoEnorm [lemma, in mathcomp.character.classfun]
+cfQuoEout [lemma, in mathcomp.character.classfun]
+cfQuoInorm [lemma, in mathcomp.character.classfun]
+cfQuoK [lemma, in mathcomp.character.classfun]
+cfQuo_irr [lemma, in mathcomp.character.character]
+cfQuo_lin_charE [lemma, in mathcomp.character.character]
+cfQuo_charE [lemma, in mathcomp.character.character]
+cfQuo_lin_char [lemma, in mathcomp.character.character]
+cfQuo_char [lemma, in mathcomp.character.character]
+cfQuo_iso [lemma, in mathcomp.character.classfun]
+cfQuo_eq1 [lemma, in mathcomp.character.classfun]
+cfQuo_cfun1 [lemma, in mathcomp.character.classfun]
+cfQuo_subproof [lemma, in mathcomp.character.classfun]
+cfQuo1 [lemma, in mathcomp.character.classfun]
+cfReal [definition, in mathcomp.character.classfun]
+cfReg [definition, in mathcomp.character.character]
+cfRegE [lemma, in mathcomp.character.character]
+cfReg_char [lemma, in mathcomp.character.character]
+cfReg_sum [lemma, in mathcomp.character.character]
+cfRepr [definition, in mathcomp.character.character]
+cfReprReg [lemma, in mathcomp.character.character]
+cfRepr_gring_center [lemma, in mathcomp.character.integral_char]
+cfRepr_morphim [lemma, in mathcomp.character.character]
+cfRepr_sub [lemma, in mathcomp.character.character]
+cfRepr_map [lemma, in mathcomp.character.character]
+cfRepr_prod [lemma, in mathcomp.character.character]
+cfRepr_char [lemma, in mathcomp.character.character]
+cfRepr_rsimP [lemma, in mathcomp.character.character]
+cfRepr_inj [lemma, in mathcomp.character.character]
+cfRepr_standard [lemma, in mathcomp.character.character]
+cfRepr_muln [lemma, in mathcomp.character.character]
+cfRepr_dsum [lemma, in mathcomp.character.character]
+cfRepr_dadd [lemma, in mathcomp.character.character]
+cfRepr_sim [lemma, in mathcomp.character.character]
+cfRepr_subproof [lemma, in mathcomp.character.character]
+cfRepr0 [lemma, in mathcomp.character.character]
+cfRepr1 [lemma, in mathcomp.character.character]
+cfRes [definition, in mathcomp.character.classfun]
+cfResE [lemma, in mathcomp.character.classfun]
+cfResEout [lemma, in mathcomp.character.classfun]
+cfResInd [lemma, in mathcomp.character.inertia]
+cfResIsom [lemma, in mathcomp.character.classfun]
+cfResMod [lemma, in mathcomp.character.classfun]
+cfResMorph [lemma, in mathcomp.character.classfun]
+cfResQuo [lemma, in mathcomp.character.classfun]
+cfResRes [lemma, in mathcomp.character.classfun]
+cfRes_vchar_on [lemma, in mathcomp.character.vcharacter]
+cfRes_vchar [lemma, in mathcomp.character.vcharacter]
+cfRes_irr_irr [lemma, in mathcomp.character.character]
+cfRes_lin_lin [lemma, in mathcomp.character.character]
+cfRes_lin_char [lemma, in mathcomp.character.character]
+cfRes_eq0 [lemma, in mathcomp.character.character]
+cfRes_char [lemma, in mathcomp.character.character]
+cfRes_prime_irr_cases [lemma, in mathcomp.character.inertia]
+cfRes_Ind_invariant [lemma, in mathcomp.character.inertia]
+cfRes_sdprodK [lemma, in mathcomp.character.classfun]
+cfRes_sub_ker [lemma, in mathcomp.character.classfun]
+cfRes_id [lemma, in mathcomp.character.classfun]
+cfRes_is_multiplicative [lemma, in mathcomp.character.classfun]
+cfRes_cfun1 [lemma, in mathcomp.character.classfun]
+cfRes_is_linear [lemma, in mathcomp.character.classfun]
+cfRes_subproof [lemma, in mathcomp.character.classfun]
+cfRes1 [lemma, in mathcomp.character.classfun]
+cfSdprod [definition, in mathcomp.character.classfun]
+cfSdprodE [lemma, in mathcomp.character.classfun]
+cfSdprodEr [lemma, in mathcomp.character.classfun]
+cfSdprodK [lemma, in mathcomp.character.classfun]
+cfSdprodKey [lemma, in mathcomp.character.classfun]
+cfSdprod_irr [lemma, in mathcomp.character.character]
+cfSdprod_lin_char [lemma, in mathcomp.character.character]
+cfSdprod_char [lemma, in mathcomp.character.character]
+cfSdprod_iso [lemma, in mathcomp.character.classfun]
+cfSdprod_eq1 [lemma, in mathcomp.character.classfun]
+cfSdprod_inj [lemma, in mathcomp.character.classfun]
+cfSdprod1 [lemma, in mathcomp.character.classfun]
+Cfun [definition, in mathcomp.character.classfun]
+cfunD1E [lemma, in mathcomp.character.classfun]
+cfunE [lemma, in mathcomp.character.classfun]
+cfunElock [lemma, in mathcomp.character.classfun]
+cfunGid [lemma, in mathcomp.character.classfun]
+cfuniE [lemma, in mathcomp.character.classfun]
+cfuniG [lemma, in mathcomp.character.classfun]
+cfuni_on [lemma, in mathcomp.character.classfun]
+cfunJ [lemma, in mathcomp.character.classfun]
+cfunJgen [lemma, in mathcomp.character.classfun]
+cfunM_on [lemma, in mathcomp.character.classfun]
+cfunM_onI [lemma, in mathcomp.character.classfun]
+CfunOrder [section, in mathcomp.character.classfun]
+CfunOrder.G [variable, in mathcomp.character.classfun]
+CfunOrder.gT [variable, in mathcomp.character.classfun]
+CfunOrder.phi [variable, in mathcomp.character.classfun]
+cfunP [lemma, in mathcomp.character.classfun]
+cfun_sum_dconstt [lemma, in mathcomp.character.vcharacter]
+cfun_sum_constt [lemma, in mathcomp.character.character]
+cfun_sum_cfdot [lemma, in mathcomp.character.character]
+cfun_irr_sum [lemma, in mathcomp.character.character]
+cfun_complement [lemma, in mathcomp.character.classfun]
+cfun_onS [lemma, in mathcomp.character.classfun]
+cfun_onG [lemma, in mathcomp.character.classfun]
+cfun_onD1 [lemma, in mathcomp.character.classfun]
+cfun_onT [lemma, in mathcomp.character.classfun]
+cfun_onE [lemma, in mathcomp.character.classfun]
+cfun_base_free [lemma, in mathcomp.character.classfun]
+cfun_on0 [lemma, in mathcomp.character.classfun]
+cfun_onP [lemma, in mathcomp.character.classfun]
+cfun_on_sum [lemma, in mathcomp.character.classfun]
+cfun_classE [lemma, in mathcomp.character.classfun]
+cfun_inP [lemma, in mathcomp.character.classfun]
+cfun_repr [lemma, in mathcomp.character.classfun]
+cfun_base [definition, in mathcomp.character.classfun]
+cfun_vectMixin [definition, in mathcomp.character.classfun]
+cfun_vect_iso [lemma, in mathcomp.character.classfun]
+cfun_scaleAr [lemma, in mathcomp.character.classfun]
+cfun_scaleAl [lemma, in mathcomp.character.classfun]
+cfun_lmodMixin [definition, in mathcomp.character.classfun]
+cfun_scaleDl [lemma, in mathcomp.character.classfun]
+cfun_scaleDr [lemma, in mathcomp.character.classfun]
+cfun_scale1 [lemma, in mathcomp.character.classfun]
+cfun_scaleA [lemma, in mathcomp.character.classfun]
+cfun_unitMixin [definition, in mathcomp.character.classfun]
+cfun_inv0id [lemma, in mathcomp.character.classfun]
+cfun_unitP [lemma, in mathcomp.character.classfun]
+cfun_mulV [lemma, in mathcomp.character.classfun]
+cfun_ringMixin [definition, in mathcomp.character.classfun]
+cfun_nz1 [lemma, in mathcomp.character.classfun]
+cfun_mulD [lemma, in mathcomp.character.classfun]
+cfun_mul1 [lemma, in mathcomp.character.classfun]
+cfun_mulC [lemma, in mathcomp.character.classfun]
+cfun_mulA [lemma, in mathcomp.character.classfun]
+cfun_zmodMixin [definition, in mathcomp.character.classfun]
+cfun_addN [lemma, in mathcomp.character.classfun]
+cfun_add0 [lemma, in mathcomp.character.classfun]
+cfun_addC [lemma, in mathcomp.character.classfun]
+cfun_addA [lemma, in mathcomp.character.classfun]
+cfun_scale [definition, in mathcomp.character.classfun]
+cfun_inv [definition, in mathcomp.character.classfun]
+cfun_unit [definition, in mathcomp.character.classfun]
+cfun_mul [definition, in mathcomp.character.classfun]
+cfun_mul_subproof [lemma, in mathcomp.character.classfun]
+cfun_indicator [definition, in mathcomp.character.classfun]
+cfun_indicator_subproof [lemma, in mathcomp.character.classfun]
+cfun_add [definition, in mathcomp.character.classfun]
+cfun_add_subproof [lemma, in mathcomp.character.classfun]
+cfun_opp [definition, in mathcomp.character.classfun]
+cfun_comp [definition, in mathcomp.character.classfun]
+cfun_comp_subproof [lemma, in mathcomp.character.classfun]
+cfun_zero [definition, in mathcomp.character.classfun]
+cfun_zero_subproof [lemma, in mathcomp.character.classfun]
+cfun_in_genP [lemma, in mathcomp.character.classfun]
+cfun_choiceMixin [definition, in mathcomp.character.classfun]
+cfun_eqMixin [definition, in mathcomp.character.classfun]
+cfun_val [projection, in mathcomp.character.classfun]
+cfun0 [lemma, in mathcomp.character.classfun]
+cfun0gen [lemma, in mathcomp.character.classfun]
+cfun0_zchar [lemma, in mathcomp.character.vcharacter]
+cfun0_char [lemma, in mathcomp.character.character]
+cfun1E [lemma, in mathcomp.character.classfun]
+cfun1Egen [lemma, in mathcomp.character.classfun]
+cfun1_vchar [lemma, in mathcomp.character.vcharacter]
+cfun1_lin_char [lemma, in mathcomp.character.character]
+cfun1_char [lemma, in mathcomp.character.character]
+cfun1_irr [lemma, in mathcomp.character.character]
+cfun11 [lemma, in mathcomp.character.classfun]
+cf_triangle_lerif [lemma, in mathcomp.character.classfun]
+CH [abbreviation, in mathcomp.solvable.center]
+ChangeOfField [section, in mathcomp.character.mxrepresentation]
+ChangeOfField.aF [variable, in mathcomp.character.mxrepresentation]
+ChangeOfField.f [variable, in mathcomp.character.mxrepresentation]
+ChangeOfField.G [variable, in mathcomp.character.mxrepresentation]
+ChangeOfField.gT [variable, in mathcomp.character.mxrepresentation]
+ChangeOfField.OneRepresentation [section, in mathcomp.character.mxrepresentation]
+ChangeOfField.OneRepresentation.n [variable, in mathcomp.character.mxrepresentation]
+ChangeOfField.OneRepresentation.rG [variable, in mathcomp.character.mxrepresentation]
+ChangeOfField.rF [variable, in mathcomp.character.mxrepresentation]
+_ ^f (ring_scope) [notation, in mathcomp.character.mxrepresentation]
+ChangeOfRing [section, in mathcomp.character.mxrepresentation]
+ChangeOfRing.aR [variable, in mathcomp.character.mxrepresentation]
+ChangeOfRing.f [variable, in mathcomp.character.mxrepresentation]
+ChangeOfRing.G [variable, in mathcomp.character.mxrepresentation]
+ChangeOfRing.gT [variable, in mathcomp.character.mxrepresentation]
+ChangeOfRing.OneRepresentation [section, in mathcomp.character.mxrepresentation]
+ChangeOfRing.OneRepresentation.n [variable, in mathcomp.character.mxrepresentation]
+ChangeOfRing.OneRepresentation.rG [variable, in mathcomp.character.mxrepresentation]
+ChangeOfRing.rR [variable, in mathcomp.character.mxrepresentation]
+_ ^f (ring_scope) [notation, in mathcomp.character.mxrepresentation]
+Char [section, in mathcomp.character.character]
+character [definition, in mathcomp.character.character]
+character [library]
+characteristic [definition, in mathcomp.fingroup.automorphism]
+Characteristicity [section, in mathcomp.fingroup.automorphism]
+Characteristicity.gT [variable, in mathcomp.fingroup.automorphism]
+_ \char _ [notation, in mathcomp.fingroup.automorphism]
+character_table_unit [lemma, in mathcomp.character.character]
+character_table [definition, in mathcomp.character.character]
+character_key [lemma, in mathcomp.character.character]
+charf_n_separable [lemma, in mathcomp.field.separable]
+charf_p_separable [lemma, in mathcomp.field.separable]
+charf0_separable [lemma, in mathcomp.field.separable]
+charI [lemma, in mathcomp.fingroup.automorphism]
+CharInjm [section, in mathcomp.fingroup.automorphism]
+CharInjm.aT [variable, in mathcomp.fingroup.automorphism]
+CharInjm.D [variable, in mathcomp.fingroup.automorphism]
+CharInjm.f [variable, in mathcomp.fingroup.automorphism]
+CharInjm.injf [variable, in mathcomp.fingroup.automorphism]
+CharInjm.rT [variable, in mathcomp.fingroup.automorphism]
+charM [lemma, in mathcomp.fingroup.automorphism]
+charP [lemma, in mathcomp.fingroup.automorphism]
+CharPoly [section, in mathcomp.algebra.mxpoly]
+CharPoly.A [variable, in mathcomp.algebra.mxpoly]
+CharPoly.diagA [variable, in mathcomp.algebra.mxpoly]
+CharPoly.n [variable, in mathcomp.algebra.mxpoly]
+CharPoly.R [variable, in mathcomp.algebra.mxpoly]
+CharPoly.size_diagA [variable, in mathcomp.algebra.mxpoly]
+CharPoly.split_diagA [variable, in mathcomp.algebra.mxpoly]
+charR [lemma, in mathcomp.solvable.commutator]
+CharSimple [section, in mathcomp.solvable.maximal]
+charsimple [definition, in mathcomp.solvable.maximal]
+charsimpleP [lemma, in mathcomp.solvable.maximal]
+charsimple_solvable [lemma, in mathcomp.solvable.maximal]
+charsimple_dprod [lemma, in mathcomp.solvable.maximal]
+CharSimple.gT [variable, in mathcomp.solvable.maximal]
+charY [lemma, in mathcomp.fingroup.automorphism]
+char_from_quotient [lemma, in mathcomp.fingroup.quotient]
+char_vchar [lemma, in mathcomp.character.vcharacter]
+char_injm [lemma, in mathcomp.fingroup.automorphism]
+char_norm [lemma, in mathcomp.fingroup.automorphism]
+char_normal [lemma, in mathcomp.fingroup.automorphism]
+char_normal_trans [lemma, in mathcomp.fingroup.automorphism]
+char_norm_trans [lemma, in mathcomp.fingroup.automorphism]
+char_sub [lemma, in mathcomp.fingroup.automorphism]
+char_norms [lemma, in mathcomp.fingroup.automorphism]
+char_trans [lemma, in mathcomp.fingroup.automorphism]
+char_refl [lemma, in mathcomp.fingroup.automorphism]
+char_poly_det [lemma, in mathcomp.algebra.mxpoly]
+char_poly_trace [lemma, in mathcomp.algebra.mxpoly]
+char_poly_monic [lemma, in mathcomp.algebra.mxpoly]
+char_poly [definition, in mathcomp.algebra.mxpoly]
+char_poly_mx [definition, in mathcomp.algebra.mxpoly]
+char_cfcenterE [lemma, in mathcomp.character.character]
+char_inv [lemma, in mathcomp.character.character]
+char_abelianP [lemma, in mathcomp.character.character]
+char_reprP [lemma, in mathcomp.character.character]
+char_sum_irr [lemma, in mathcomp.character.character]
+char_sum_irrP [lemma, in mathcomp.character.character]
+char_Fp_0 [lemma, in mathcomp.algebra.zmodp]
+char_Fp [lemma, in mathcomp.algebra.zmodp]
+char_Zp [lemma, in mathcomp.algebra.zmodp]
+Char.G [variable, in mathcomp.character.character]
+Char.gT [variable, in mathcomp.character.character]
+Char.StandardRepr [section, in mathcomp.character.character]
+Char.StandardRepr.iG [variable, in mathcomp.character.character]
+Char.StandardRepr.n [variable, in mathcomp.character.character]
+Char.StandardRepr.rG [variable, in mathcomp.character.character]
+Char.StandardRepr.sG [variable, in mathcomp.character.character]
+char0_PET [lemma, in mathcomp.field.separable]
+char1 [lemma, in mathcomp.fingroup.automorphism]
+char1_ge_constt [lemma, in mathcomp.character.character]
+char1_ge_norm [lemma, in mathcomp.character.character]
+char1_gt0 [lemma, in mathcomp.character.character]
+char1_eq0 [lemma, in mathcomp.character.character]
+char1_ge0 [lemma, in mathcomp.character.character]
+Chiefs [section, in mathcomp.solvable.gseries]
+Chiefs.gT [variable, in mathcomp.solvable.gseries]
+chief_series_exists [lemma, in mathcomp.solvable.gseries]
+chief_factor_minnormal [lemma, in mathcomp.solvable.gseries]
+chief_factor [definition, in mathcomp.solvable.gseries]
+chinese [definition, in mathcomp.ssreflect.div]
+Chinese [section, in mathcomp.ssreflect.div]
+Chinese [section, in mathcomp.algebra.intdiv]
+chinese_mod [lemma, in mathcomp.ssreflect.div]
+chinese_modr [lemma, in mathcomp.ssreflect.div]
+chinese_modl [lemma, in mathcomp.ssreflect.div]
+chinese_remainder [lemma, in mathcomp.ssreflect.div]
+Chinese.co_m12 [variable, in mathcomp.ssreflect.div]
+Chinese.co_m12 [variable, in mathcomp.algebra.intdiv]
+Chinese.m1 [variable, in mathcomp.ssreflect.div]
+Chinese.m1 [variable, in mathcomp.algebra.intdiv]
+Chinese.m2 [variable, in mathcomp.ssreflect.div]
+Chinese.m2 [variable, in mathcomp.algebra.intdiv]
+Choice [module, in mathcomp.ssreflect.choice]
+choice [library]
+ChoiceTheory [section, in mathcomp.ssreflect.choice]
+ChoiceTheory.OneType [section, in mathcomp.ssreflect.choice]
+ChoiceTheory.OneType.CanChoice [section, in mathcomp.ssreflect.choice]
+ChoiceTheory.OneType.CanChoice.f [variable, in mathcomp.ssreflect.choice]
+ChoiceTheory.OneType.CanChoice.sT [variable, in mathcomp.ssreflect.choice]
+ChoiceTheory.OneType.SubChoice [section, in mathcomp.ssreflect.choice]
+ChoiceTheory.OneType.SubChoice.P [variable, in mathcomp.ssreflect.choice]
+ChoiceTheory.OneType.SubChoice.sT [variable, in mathcomp.ssreflect.choice]
+ChoiceTheory.OneType.T [variable, in mathcomp.ssreflect.choice]
+ChoiceTheory.TagChoice [section, in mathcomp.ssreflect.choice]
+ChoiceTheory.TagChoice.I [variable, in mathcomp.ssreflect.choice]
+ChoiceTheory.TagChoice.T_ [variable, in mathcomp.ssreflect.choice]
+Choice.base [projection, in mathcomp.ssreflect.choice]
+Choice.class [definition, in mathcomp.ssreflect.choice]
+Choice.Class [constructor, in mathcomp.ssreflect.choice]
+Choice.ClassDef [section, in mathcomp.ssreflect.choice]
+Choice.ClassDef.cT [variable, in mathcomp.ssreflect.choice]
+Choice.ClassDef.T [variable, in mathcomp.ssreflect.choice]
+Choice.ClassDef.xT [variable, in mathcomp.ssreflect.choice]
+Choice.class_of [record, in mathcomp.ssreflect.choice]
+Choice.clone [definition, in mathcomp.ssreflect.choice]
+Choice.eqType [definition, in mathcomp.ssreflect.choice]
+Choice.Exports [module, in mathcomp.ssreflect.choice]
+Choice.Exports.choiceMixin [abbreviation, in mathcomp.ssreflect.choice]
+Choice.Exports.ChoiceType [abbreviation, in mathcomp.ssreflect.choice]
+Choice.Exports.choiceType [abbreviation, in mathcomp.ssreflect.choice]
+[ choiceType of _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
+[ choiceType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
+Choice.find [projection, in mathcomp.ssreflect.choice]
+Choice.InternalTheory [module, in mathcomp.ssreflect.choice]
+Choice.InternalTheory.complete [lemma, in mathcomp.ssreflect.choice]
+Choice.InternalTheory.correct [lemma, in mathcomp.ssreflect.choice]
+Choice.InternalTheory.extensional [lemma, in mathcomp.ssreflect.choice]
+Choice.InternalTheory.find [definition, in mathcomp.ssreflect.choice]
+Choice.InternalTheory.InternalTheory [section, in mathcomp.ssreflect.choice]
+Choice.InternalTheory.InternalTheory.T [variable, in mathcomp.ssreflect.choice]
+Choice.InternalTheory.xchoose_subproof [lemma, in mathcomp.ssreflect.choice]
+Choice.mixin [projection, in mathcomp.ssreflect.choice]
+Choice.Mixin [constructor, in mathcomp.ssreflect.choice]
+Choice.mixin_of [record, in mathcomp.ssreflect.choice]
+Choice.pack [definition, in mathcomp.ssreflect.choice]
+Choice.Pack [constructor, in mathcomp.ssreflect.choice]
+Choice.sort [projection, in mathcomp.ssreflect.choice]
+Choice.type [record, in mathcomp.ssreflect.choice]
+Choice.xclass [abbreviation, in mathcomp.ssreflect.choice]
+choose [definition, in mathcomp.ssreflect.choice]
+chooseP [lemma, in mathcomp.ssreflect.choice]
+choose_id [lemma, in mathcomp.ssreflect.choice]
+CintE [lemma, in mathcomp.field.algC]
+CintEge0 [lemma, in mathcomp.field.algC]
+CintEsign [lemma, in mathcomp.field.algC]
+CintP [lemma, in mathcomp.field.algC]
+CintrE [definition, in mathcomp.field.algC]
+Cintr_Cyclotomic [lemma, in mathcomp.field.cyclotomic]
+Cint_aut [lemma, in mathcomp.field.algC]
+Cint_rat [lemma, in mathcomp.field.algC]
+Cint_ler_sqr [lemma, in mathcomp.field.algC]
+Cint_Cnat [lemma, in mathcomp.field.algC]
+Cint_normK [lemma, in mathcomp.field.algC]
+Cint_subring [lemma, in mathcomp.field.algC]
+Cint_key [lemma, in mathcomp.field.algC]
+Cint_int [lemma, in mathcomp.field.algC]
+Cint_cfdot_vchar [lemma, in mathcomp.character.vcharacter]
+Cint_cfdot_vchar_irr [lemma, in mathcomp.character.vcharacter]
+Cint_vchar1 [lemma, in mathcomp.character.vcharacter]
+Cint_rat_Aint [lemma, in mathcomp.field.algnum]
+Cint_span_zmod_closed [lemma, in mathcomp.field.algnum]
+Cint_spanP [lemma, in mathcomp.field.algnum]
+Cint_span_key [lemma, in mathcomp.field.algnum]
+Cint_span [definition, in mathcomp.field.algnum]
+Cint0 [lemma, in mathcomp.field.algC]
+Cint1 [lemma, in mathcomp.field.algC]
+CK [abbreviation, in mathcomp.solvable.center]
+class [definition, in mathcomp.fingroup.fingroup]
+classes [definition, in mathcomp.fingroup.fingroup]
+classes_quotient [lemma, in mathcomp.fingroup.quotient]
+classes_partition [lemma, in mathcomp.fingroup.action]
+classes_morphim [lemma, in mathcomp.fingroup.morphism]
+classes_gt1 [lemma, in mathcomp.fingroup.fingroup]
+classes_gt0 [lemma, in mathcomp.fingroup.fingroup]
+classes1 [lemma, in mathcomp.fingroup.fingroup]
+ClassFun [section, in mathcomp.character.classfun]
+classfun [record, in mathcomp.character.classfun]
+Classfun [constructor, in mathcomp.character.classfun]
+classfun [library]
+classfun_on [definition, in mathcomp.character.classfun]
+classfun_key [lemma, in mathcomp.character.classfun]
+ClassFun.G [variable, in mathcomp.character.classfun]
+ClassFun.gT [variable, in mathcomp.character.classfun]
+'1_ _ [notation, in mathcomp.character.classfun]
+classGidl [lemma, in mathcomp.fingroup.fingroup]
+classGidr [lemma, in mathcomp.fingroup.fingroup]
+classg_base_center [lemma, in mathcomp.character.mxrepresentation]
+classg_base_free [lemma, in mathcomp.character.mxrepresentation]
+classg_base [definition, in mathcomp.character.mxrepresentation]
+classG_eq1 [lemma, in mathcomp.fingroup.fingroup]
+classM [lemma, in mathcomp.fingroup.fingroup]
+classS [lemma, in mathcomp.fingroup.fingroup]
+classVg [lemma, in mathcomp.fingroup.fingroup]
+class_IirrK [lemma, in mathcomp.character.character]
+class_Iirr [definition, in mathcomp.character.character]
+class_formula [lemma, in mathcomp.fingroup.action]
+class_support_sub_norm [lemma, in mathcomp.fingroup.fingroup]
+class_support_norm [lemma, in mathcomp.fingroup.fingroup]
+class_sub_norm [lemma, in mathcomp.fingroup.fingroup]
+class_normal [lemma, in mathcomp.fingroup.fingroup]
+class_norm [lemma, in mathcomp.fingroup.fingroup]
+class_supportD1 [lemma, in mathcomp.fingroup.fingroup]
+class_support_id [lemma, in mathcomp.fingroup.fingroup]
+class_support_subG [lemma, in mathcomp.fingroup.fingroup]
+class_supportGidr [lemma, in mathcomp.fingroup.fingroup]
+class_supportGidl [lemma, in mathcomp.fingroup.fingroup]
+class_subG [lemma, in mathcomp.fingroup.fingroup]
+class_trans [lemma, in mathcomp.fingroup.fingroup]
+class_transl [lemma, in mathcomp.fingroup.fingroup]
+class_sym [lemma, in mathcomp.fingroup.fingroup]
+class_eqP [lemma, in mathcomp.fingroup.fingroup]
+class_refl [lemma, in mathcomp.fingroup.fingroup]
+class_supportEr [lemma, in mathcomp.fingroup.fingroup]
+class_supportEl [lemma, in mathcomp.fingroup.fingroup]
+class_rcoset [lemma, in mathcomp.fingroup.fingroup]
+class_lcoset [lemma, in mathcomp.fingroup.fingroup]
+class_support_set1r [lemma, in mathcomp.fingroup.fingroup]
+class_support_set1l [lemma, in mathcomp.fingroup.fingroup]
+class_supportM [lemma, in mathcomp.fingroup.fingroup]
+class_set1 [lemma, in mathcomp.fingroup.fingroup]
+class_support [definition, in mathcomp.fingroup.fingroup]
+class1G [lemma, in mathcomp.fingroup.fingroup]
+class1g [lemma, in mathcomp.fingroup.fingroup]
+Clifford_rstabs_simple [lemma, in mathcomp.character.mxrepresentation]
+Clifford_astab1 [lemma, in mathcomp.character.mxrepresentation]
+Clifford_astab [lemma, in mathcomp.character.mxrepresentation]
+Clifford_component_basis [lemma, in mathcomp.character.mxrepresentation]
+Clifford_rank_components [lemma, in mathcomp.character.mxrepresentation]
+Clifford_Socle1 [lemma, in mathcomp.character.mxrepresentation]
+Clifford_atrans [lemma, in mathcomp.character.mxrepresentation]
+Clifford_action [definition, in mathcomp.character.mxrepresentation]
+Clifford_is_action [lemma, in mathcomp.character.mxrepresentation]
+Clifford_act [definition, in mathcomp.character.mxrepresentation]
+Clifford_basis [lemma, in mathcomp.character.mxrepresentation]
+Clifford_componentJ [lemma, in mathcomp.character.mxrepresentation]
+Clifford_iso2 [lemma, in mathcomp.character.mxrepresentation]
+Clifford_iso [lemma, in mathcomp.character.mxrepresentation]
+Clifford_hom [lemma, in mathcomp.character.mxrepresentation]
+Clifford_simple [lemma, in mathcomp.character.mxrepresentation]
+Clifford_Res_sum_cfclass [lemma, in mathcomp.character.inertia]
+clone_groupAction [definition, in mathcomp.fingroup.action]
+clone_action [definition, in mathcomp.fingroup.action]
+clone_subType [definition, in mathcomp.ssreflect.eqtype]
+clone_morphism [definition, in mathcomp.fingroup.morphism]
+clone_group [definition, in mathcomp.fingroup.fingroup]
+clone_aspace [definition, in mathcomp.field.falgebra]
+closed [abbreviation, in mathcomp.ssreflect.fingraph]
+ClosedField [section, in mathcomp.algebra.poly]
+ClosedFieldQE [section, in mathcomp.field.closed_field]
+ClosedFieldQE.axiom [variable, in mathcomp.field.closed_field]
+ClosedFieldQE.F [variable, in mathcomp.field.closed_field]
+ClosedField.closedF [variable, in mathcomp.algebra.poly]
+ClosedField.F [variable, in mathcomp.algebra.poly]
+closed_field_poly_normal [lemma, in mathcomp.algebra.poly]
+closed_nonrootP [lemma, in mathcomp.algebra.poly]
+closed_rootP [lemma, in mathcomp.algebra.poly]
+closed_fields_QEMixin [definition, in mathcomp.field.closed_field]
+closed_connect [lemma, in mathcomp.ssreflect.fingraph]
+closed_mem [definition, in mathcomp.ssreflect.fingraph]
+closed_field [library]
+Closure [section, in mathcomp.ssreflect.fingraph]
+closure [abbreviation, in mathcomp.ssreflect.fingraph]
+Closure [section, in mathcomp.field.falgebra]
+closure_closed [lemma, in mathcomp.ssreflect.fingraph]
+closure_mem [definition, in mathcomp.ssreflect.fingraph]
+Closure.aT [variable, in mathcomp.field.falgebra]
+Closure.e [variable, in mathcomp.ssreflect.fingraph]
+Closure.K [variable, in mathcomp.field.falgebra]
+Closure.sym_e [variable, in mathcomp.ssreflect.fingraph]
+Closure.T [variable, in mathcomp.ssreflect.fingraph]
+<< _ ; _ >> (vspace_scope) [notation, in mathcomp.field.falgebra]
+<< _ & _ >> (vspace_scope) [notation, in mathcomp.field.falgebra]
+CnatEint [lemma, in mathcomp.field.algC]
+CnatP [lemma, in mathcomp.field.algC]
+Cnat_aut [lemma, in mathcomp.field.algC]
+Cnat_exp_even [lemma, in mathcomp.field.algC]
+Cnat_norm_Cint [lemma, in mathcomp.field.algC]
+Cnat_prod_eq1 [lemma, in mathcomp.field.algC]
+Cnat_mul_eq1 [lemma, in mathcomp.field.algC]
+Cnat_sum_eq1 [lemma, in mathcomp.field.algC]
+Cnat_gt0 [lemma, in mathcomp.field.algC]
+Cnat_ge0 [lemma, in mathcomp.field.algC]
+Cnat_semiring [lemma, in mathcomp.field.algC]
+Cnat_key [lemma, in mathcomp.field.algC]
+Cnat_nat [lemma, in mathcomp.field.algC]
+Cnat_dirr [lemma, in mathcomp.character.vcharacter]
+Cnat_cfnorm_vchar [lemma, in mathcomp.character.vcharacter]
+Cnat_cfdot_char [lemma, in mathcomp.character.character]
+Cnat_cfdot_char_irr [lemma, in mathcomp.character.character]
+Cnat_char1 [lemma, in mathcomp.character.character]
+Cnat_irr1 [lemma, in mathcomp.character.character]
+Cnat0 [lemma, in mathcomp.field.algC]
+Cnat1 [lemma, in mathcomp.field.algC]
+cnorm_dconstt [lemma, in mathcomp.character.vcharacter]
+CodeSeq [module, in mathcomp.ssreflect.choice]
+CodeSeq.code [definition, in mathcomp.ssreflect.choice]
+CodeSeq.codeK [lemma, in mathcomp.ssreflect.choice]
+CodeSeq.decode [definition, in mathcomp.ssreflect.choice]
+CodeSeq.decodeK [lemma, in mathcomp.ssreflect.choice]
+CodeSeq.decode_rec [definition, in mathcomp.ssreflect.choice]
+CodeSeq.gtn_decode [lemma, in mathcomp.ssreflect.choice]
+CodeSeq.ltn_code [lemma, in mathcomp.ssreflect.choice]
+[ rec _ , _ , _ ] [notation, in mathcomp.ssreflect.choice]
+codom [definition, in mathcomp.ssreflect.fintype]
+codomE [lemma, in mathcomp.ssreflect.fintype]
+codomP [lemma, in mathcomp.ssreflect.fintype]
+codom_val [lemma, in mathcomp.ssreflect.fintype]
+codom_f [lemma, in mathcomp.ssreflect.fintype]
+codom_ffun [lemma, in mathcomp.ssreflect.finfun]
+coefB [lemma, in mathcomp.algebra.poly]
+coefC [lemma, in mathcomp.algebra.poly]
+coefCM [lemma, in mathcomp.algebra.poly]
+coefD [lemma, in mathcomp.algebra.poly]
+coefK [lemma, in mathcomp.algebra.poly]
+coefM [lemma, in mathcomp.algebra.poly]
+coefMC [lemma, in mathcomp.algebra.poly]
+coefMn [lemma, in mathcomp.algebra.poly]
+coefMNn [lemma, in mathcomp.algebra.poly]
+coefMr [lemma, in mathcomp.algebra.poly]
+coefMrz [lemma, in mathcomp.algebra.ssrint]
+coefMX [lemma, in mathcomp.algebra.poly]
+coefMXn [lemma, in mathcomp.algebra.poly]
+coefN [lemma, in mathcomp.algebra.poly]
+coefp [abbreviation, in mathcomp.algebra.poly]
+coefp_head [definition, in mathcomp.algebra.poly]
+coefp0_multiplicative [lemma, in mathcomp.algebra.poly]
+coefX [lemma, in mathcomp.algebra.poly]
+coefXM [lemma, in mathcomp.algebra.poly]
+coefXn [lemma, in mathcomp.algebra.poly]
+coefXnM [lemma, in mathcomp.algebra.poly]
+coefZ [lemma, in mathcomp.algebra.poly]
+coef_rVpoly_ord [lemma, in mathcomp.algebra.mxpoly]
+coef_rVpoly [lemma, in mathcomp.algebra.mxpoly]
+coef_swapXY [lemma, in mathcomp.algebra.polyXY]
+coef_map [lemma, in mathcomp.algebra.poly]
+coef_map_id0 [lemma, in mathcomp.algebra.poly]
+coef_nderivn [lemma, in mathcomp.algebra.poly]
+coef_derivn [lemma, in mathcomp.algebra.poly]
+coef_deriv [lemma, in mathcomp.algebra.poly]
+coef_mul_poly_rev [lemma, in mathcomp.algebra.poly]
+coef_mul_poly [lemma, in mathcomp.algebra.poly]
+coef_sum [lemma, in mathcomp.algebra.poly]
+coef_opp_poly [lemma, in mathcomp.algebra.poly]
+coef_add_poly [lemma, in mathcomp.algebra.poly]
+coef_poly [lemma, in mathcomp.algebra.poly]
+coef_Poly [lemma, in mathcomp.algebra.poly]
+coef_cons [lemma, in mathcomp.algebra.poly]
+coef0 [lemma, in mathcomp.algebra.poly]
+coef1 [lemma, in mathcomp.algebra.poly]
+coerced_frel [abbreviation, in mathcomp.ssreflect.eqtype]
+cofactor [definition, in mathcomp.algebra.matrix]
+cofactorZ [lemma, in mathcomp.algebra.matrix]
+cofactor_tr [lemma, in mathcomp.algebra.matrix]
+cofactor_map_mx [lemma, in mathcomp.algebra.matrix]
+coin0 [definition, in mathcomp.solvable.burnside_app]
+coin1 [definition, in mathcomp.solvable.burnside_app]
+coin2 [definition, in mathcomp.solvable.burnside_app]
+coin3 [definition, in mathcomp.solvable.burnside_app]
+cokermx [definition, in mathcomp.algebra.mxalgebra]
+cokermx_eq0 [lemma, in mathcomp.algebra.mxalgebra]
+col [definition, in mathcomp.algebra.matrix]
+colKl [lemma, in mathcomp.algebra.matrix]
+colKr [lemma, in mathcomp.algebra.matrix]
+colors [definition, in mathcomp.solvable.burnside_app]
+colouring [section, in mathcomp.solvable.burnside_app]
+colouring.cube_colouring [section, in mathcomp.solvable.burnside_app]
+colouring.n [variable, in mathcomp.solvable.burnside_app]
+colouring.square_colouring [section, in mathcomp.solvable.burnside_app]
+colP [lemma, in mathcomp.algebra.matrix]
+col_permE [lemma, in mathcomp.algebra.matrix]
+col_mx_eq0 [lemma, in mathcomp.algebra.matrix]
+col_mx0 [lemma, in mathcomp.algebra.matrix]
+col_col_mx [lemma, in mathcomp.algebra.matrix]
+col_mxAx [definition, in mathcomp.algebra.matrix]
+col_mxA [lemma, in mathcomp.algebra.matrix]
+col_mx_const [lemma, in mathcomp.algebra.matrix]
+col_mxKd [lemma, in mathcomp.algebra.matrix]
+col_mxEd [lemma, in mathcomp.algebra.matrix]
+col_mxKu [lemma, in mathcomp.algebra.matrix]
+col_mxEu [lemma, in mathcomp.algebra.matrix]
+col_mx [definition, in mathcomp.algebra.matrix]
+col_mx_key [lemma, in mathcomp.algebra.matrix]
+col_eq [lemma, in mathcomp.algebra.matrix]
+col_id [lemma, in mathcomp.algebra.matrix]
+col_row_permC [lemma, in mathcomp.algebra.matrix]
+col_permM [lemma, in mathcomp.algebra.matrix]
+col_perm1 [lemma, in mathcomp.algebra.matrix]
+col_const [lemma, in mathcomp.algebra.matrix]
+col_perm_const [lemma, in mathcomp.algebra.matrix]
+col_perm [definition, in mathcomp.algebra.matrix]
+col_perm_key [lemma, in mathcomp.algebra.matrix]
+col_mx_sub [lemma, in mathcomp.algebra.mxalgebra]
+col_base_full [lemma, in mathcomp.algebra.mxalgebra]
+col_ebase_unit [lemma, in mathcomp.algebra.mxalgebra]
+col_leq_rank [lemma, in mathcomp.algebra.mxalgebra]
+col_base [definition, in mathcomp.algebra.mxalgebra]
+col_ebase [definition, in mathcomp.algebra.mxalgebra]
+col_cubes [abbreviation, in mathcomp.solvable.burnside_app]
+col_squares [abbreviation, in mathcomp.solvable.burnside_app]
+col' [definition, in mathcomp.algebra.matrix]
+col'Kl [lemma, in mathcomp.algebra.matrix]
+col'Kr [lemma, in mathcomp.algebra.matrix]
+col'_col_mx [lemma, in mathcomp.algebra.matrix]
+col'_eq [lemma, in mathcomp.algebra.matrix]
+col'_const [lemma, in mathcomp.algebra.matrix]
+col0 [lemma, in mathcomp.algebra.matrix]
+col0 [definition, in mathcomp.solvable.burnside_app]
+col1 [definition, in mathcomp.solvable.burnside_app]
+col2 [definition, in mathcomp.solvable.burnside_app]
+col3 [definition, in mathcomp.solvable.burnside_app]
+col4 [definition, in mathcomp.solvable.burnside_app]
+col5 [definition, in mathcomp.solvable.burnside_app]
+Combinations [section, in mathcomp.ssreflect.binomial]
+ComMatrix [section, in mathcomp.algebra.matrix]
+ComMatrix.AssocLeft [section, in mathcomp.algebra.matrix]
+ComMatrix.AssocLeft.m [variable, in mathcomp.algebra.matrix]
+ComMatrix.AssocLeft.n [variable, in mathcomp.algebra.matrix]
+ComMatrix.AssocLeft.p [variable, in mathcomp.algebra.matrix]
+ComMatrix.LinMulRow [section, in mathcomp.algebra.matrix]
+ComMatrix.LinMulRow.m [variable, in mathcomp.algebra.matrix]
+ComMatrix.LinMulRow.n [variable, in mathcomp.algebra.matrix]
+ComMatrix.MatrixAlgType [section, in mathcomp.algebra.matrix]
+ComMatrix.MatrixAlgType.n' [variable, in mathcomp.algebra.matrix]
+ComMatrix.R [variable, in mathcomp.algebra.matrix]
+commg [definition, in mathcomp.fingroup.fingroup]
+commgAC [lemma, in mathcomp.solvable.commutator]
+commGC [lemma, in mathcomp.fingroup.fingroup]
+commgC [lemma, in mathcomp.fingroup.fingroup]
+commgCV [lemma, in mathcomp.fingroup.fingroup]
+commgEl [lemma, in mathcomp.fingroup.fingroup]
+commgEr [lemma, in mathcomp.fingroup.fingroup]
+commgg [lemma, in mathcomp.fingroup.fingroup]
+commgMJ [lemma, in mathcomp.solvable.commutator]
+commgMR [lemma, in mathcomp.solvable.commutator]
+commgP [lemma, in mathcomp.fingroup.fingroup]
+commgS [lemma, in mathcomp.fingroup.fingroup]
+commgSS [lemma, in mathcomp.fingroup.fingroup]
+commgV [lemma, in mathcomp.solvable.commutator]
+commgVg [lemma, in mathcomp.fingroup.fingroup]
+commgX [lemma, in mathcomp.solvable.commutator]
+commgXg [lemma, in mathcomp.fingroup.fingroup]
+commgXVg [lemma, in mathcomp.fingroup.fingroup]
+commg_normSr [lemma, in mathcomp.solvable.commutator]
+commg_normSl [lemma, in mathcomp.solvable.commutator]
+commg_subI [lemma, in mathcomp.solvable.commutator]
+commg_subl [lemma, in mathcomp.solvable.commutator]
+commg_subr [lemma, in mathcomp.solvable.commutator]
+commg_normal [lemma, in mathcomp.solvable.commutator]
+commg_norm [lemma, in mathcomp.solvable.commutator]
+commg_normr [lemma, in mathcomp.solvable.commutator]
+commg_norml [lemma, in mathcomp.solvable.commutator]
+commg_sub [lemma, in mathcomp.solvable.commutator]
+commg_set [definition, in mathcomp.fingroup.fingroup]
+commG1 [lemma, in mathcomp.solvable.commutator]
+commg1 [lemma, in mathcomp.fingroup.fingroup]
+commG1P [lemma, in mathcomp.fingroup.fingroup]
+commg1_sym [lemma, in mathcomp.fingroup.fingroup]
+commMG [lemma, in mathcomp.solvable.commutator]
+commMgJ [lemma, in mathcomp.solvable.commutator]
+commMGr [lemma, in mathcomp.solvable.commutator]
+commMgR [lemma, in mathcomp.solvable.commutator]
+commrMz [lemma, in mathcomp.algebra.ssrint]
+commrXz [lemma, in mathcomp.algebra.ssrint]
+commrXz_wmulls [lemma, in mathcomp.algebra.ssrint]
+commr_rmorph [definition, in mathcomp.algebra.poly]
+commr_polyXn [lemma, in mathcomp.algebra.poly]
+commr_polyX [lemma, in mathcomp.algebra.poly]
+commr_int [lemma, in mathcomp.algebra.ssrint]
+commSg [lemma, in mathcomp.fingroup.fingroup]
+commutator [definition, in mathcomp.fingroup.fingroup]
+commutator [library]
+Commutator_properties.gT [variable, in mathcomp.solvable.commutator]
+Commutator_properties [section, in mathcomp.solvable.commutator]
+commute [definition, in mathcomp.fingroup.fingroup]
+commuteM [lemma, in mathcomp.fingroup.fingroup]
+commuteV [lemma, in mathcomp.fingroup.fingroup]
+commuteX [lemma, in mathcomp.fingroup.fingroup]
+commuteX2 [lemma, in mathcomp.fingroup.fingroup]
+commute_sym [lemma, in mathcomp.fingroup.fingroup]
+commute_refl [lemma, in mathcomp.fingroup.fingroup]
+commute1 [lemma, in mathcomp.fingroup.fingroup]
+commVg [lemma, in mathcomp.solvable.commutator]
+commXg [lemma, in mathcomp.solvable.commutator]
+commXXg [lemma, in mathcomp.solvable.commutator]
+comm_sub_max_pgroup [lemma, in mathcomp.solvable.pgroup]
+comm_polyX [lemma, in mathcomp.algebra.poly]
+comm_poly1 [lemma, in mathcomp.algebra.poly]
+comm_poly0 [lemma, in mathcomp.algebra.poly]
+comm_coef_poly [lemma, in mathcomp.algebra.poly]
+comm_poly [definition, in mathcomp.algebra.poly]
+comm_coef [definition, in mathcomp.algebra.poly]
+comm_norm_cent_cent [lemma, in mathcomp.solvable.commutator]
+comm_subG [lemma, in mathcomp.fingroup.fingroup]
+comm_joingE [lemma, in mathcomp.fingroup.fingroup]
+comm_group_setP [lemma, in mathcomp.fingroup.fingroup]
+comm1G [lemma, in mathcomp.solvable.commutator]
+comm1g [lemma, in mathcomp.fingroup.fingroup]
+comm3G1P [lemma, in mathcomp.solvable.commutator]
+CompAct [section, in mathcomp.fingroup.action]
+CompAct.aT [variable, in mathcomp.fingroup.action]
+CompAct.B [variable, in mathcomp.fingroup.action]
+CompAct.D [variable, in mathcomp.fingroup.action]
+CompAct.f [variable, in mathcomp.fingroup.action]
+CompAct.gT [variable, in mathcomp.fingroup.action]
+CompAct.rT [variable, in mathcomp.fingroup.action]
+CompAct.to [variable, in mathcomp.fingroup.action]
+comparable [definition, in mathcomp.ssreflect.eqtype]
+comparableClass [definition, in mathcomp.ssreflect.eqtype]
+ComparableType [section, in mathcomp.ssreflect.eqtype]
+ComparableType.Hcompare [variable, in mathcomp.ssreflect.eqtype]
+ComparableType.T [variable, in mathcomp.ssreflect.eqtype]
+compareb [definition, in mathcomp.ssreflect.eqtype]
+CompareNatEq [constructor, in mathcomp.ssreflect.ssrnat]
+CompareNatGt [constructor, in mathcomp.ssreflect.ssrnat]
+CompareNatLt [constructor, in mathcomp.ssreflect.ssrnat]
+compareP [lemma, in mathcomp.ssreflect.eqtype]
+compare_nat [inductive, in mathcomp.ssreflect.ssrnat]
+complements_to_in [definition, in mathcomp.fingroup.gproduct]
+complete_unitmx [lemma, in mathcomp.algebra.mxalgebra]
+ComplexNumMixin [lemma, in mathcomp.field.algC]
+CompLfun [section, in mathcomp.algebra.vector]
+CompLfun.aT [variable, in mathcomp.algebra.vector]
+CompLfun.R [variable, in mathcomp.algebra.vector]
+CompLfun.rT [variable, in mathcomp.algebra.vector]
+CompLfun.vT [variable, in mathcomp.algebra.vector]
+CompLfun.wT [variable, in mathcomp.algebra.vector]
+complgC [lemma, in mathcomp.fingroup.gproduct]
+complmx [definition, in mathcomp.algebra.mxalgebra]
+complP [lemma, in mathcomp.fingroup.gproduct]
+complv [definition, in mathcomp.algebra.vector]
+compl_p'Hall [lemma, in mathcomp.solvable.pgroup]
+compl_pHall [lemma, in mathcomp.solvable.pgroup]
+compo [abbreviation, in mathcomp.solvable.jordanholder]
+component_socle [lemma, in mathcomp.character.mxrepresentation]
+component_mx_disjoint [lemma, in mathcomp.character.mxrepresentation]
+component_mx_isoP [lemma, in mathcomp.character.mxrepresentation]
+component_mx_iso [lemma, in mathcomp.character.mxrepresentation]
+component_mx_id [lemma, in mathcomp.character.mxrepresentation]
+component_mx_semisimple [lemma, in mathcomp.character.mxrepresentation]
+component_mx_def [lemma, in mathcomp.character.mxrepresentation]
+component_mx_module [lemma, in mathcomp.character.mxrepresentation]
+component_mx [definition, in mathcomp.character.mxrepresentation]
+component_mx_expr [definition, in mathcomp.character.mxrepresentation]
+component_mx_key [lemma, in mathcomp.character.mxrepresentation]
+CompositionSeries [section, in mathcomp.solvable.jordanholder]
+CompositionSeries.gT [variable, in mathcomp.solvable.jordanholder]
+comps [definition, in mathcomp.solvable.jordanholder]
+compsP [lemma, in mathcomp.solvable.jordanholder]
+comps_cons [lemma, in mathcomp.solvable.jordanholder]
+compU [abbreviation, in mathcomp.character.mxrepresentation]
+comp_kHom [lemma, in mathcomp.field.galois]
+comp_kHom_img [lemma, in mathcomp.field.galois]
+comp_lfunZr [lemma, in mathcomp.algebra.vector]
+comp_lfunZl [lemma, in mathcomp.algebra.vector]
+comp_lfunNr [lemma, in mathcomp.algebra.vector]
+comp_lfunNl [lemma, in mathcomp.algebra.vector]
+comp_lfunDr [lemma, in mathcomp.algebra.vector]
+comp_lfunDl [lemma, in mathcomp.algebra.vector]
+comp_lfun0r [lemma, in mathcomp.algebra.vector]
+comp_lfun0l [lemma, in mathcomp.algebra.vector]
+comp_lfun1r [lemma, in mathcomp.algebra.vector]
+comp_lfun1l [lemma, in mathcomp.algebra.vector]
+comp_lfunA [lemma, in mathcomp.algebra.vector]
+comp_lfunE [lemma, in mathcomp.algebra.vector]
+comp_lfun [definition, in mathcomp.algebra.vector]
+comp_is_groupAction [lemma, in mathcomp.fingroup.action]
+comp_actE [lemma, in mathcomp.fingroup.action]
+comp_is_action [lemma, in mathcomp.fingroup.action]
+comp_act [definition, in mathcomp.fingroup.action]
+comp_poly2_eq0 [lemma, in mathcomp.algebra.poly]
+comp_polyA [lemma, in mathcomp.algebra.poly]
+comp_polyM [lemma, in mathcomp.algebra.poly]
+comp_poly_multiplicative [lemma, in mathcomp.algebra.poly]
+comp_polyXaddC_K [lemma, in mathcomp.algebra.poly]
+comp_poly_MXaddC [lemma, in mathcomp.algebra.poly]
+comp_polyX [lemma, in mathcomp.algebra.poly]
+comp_polyXr [lemma, in mathcomp.algebra.poly]
+comp_polyZ [lemma, in mathcomp.algebra.poly]
+comp_polyB [lemma, in mathcomp.algebra.poly]
+comp_polyD [lemma, in mathcomp.algebra.poly]
+comp_poly0 [lemma, in mathcomp.algebra.poly]
+comp_poly_is_linear [lemma, in mathcomp.algebra.poly]
+comp_polyC [lemma, in mathcomp.algebra.poly]
+comp_poly0r [lemma, in mathcomp.algebra.poly]
+comp_polyCr [lemma, in mathcomp.algebra.poly]
+comp_polyE [lemma, in mathcomp.algebra.poly]
+comp_poly [definition, in mathcomp.algebra.poly]
+comp_reprGLm [lemma, in mathcomp.character.mxabelem]
+comp_morphM [lemma, in mathcomp.fingroup.morphism]
+comp_is_ahom [lemma, in mathcomp.field.falgebra]
+conform_castmx [lemma, in mathcomp.algebra.matrix]
+conform_mx_id [lemma, in mathcomp.algebra.matrix]
+conform_mx [definition, in mathcomp.algebra.matrix]
+congr_subvs [lemma, in mathcomp.algebra.vector]
+congr_irr [lemma, in mathcomp.character.character]
+congr_big_nat [lemma, in mathcomp.ssreflect.bigop]
+congr_big [lemma, in mathcomp.ssreflect.bigop]
+congr_subg [lemma, in mathcomp.fingroup.fingroup]
+congr_group [lemma, in mathcomp.fingroup.fingroup]
+Conj [section, in mathcomp.character.inertia]
+conjCg [lemma, in mathcomp.fingroup.fingroup]
+conjC_vcharAut [lemma, in mathcomp.character.vcharacter]
+conjC_Iirr_eq0 [lemma, in mathcomp.character.character]
+conjC_Iirr0 [lemma, in mathcomp.character.character]
+conjC_IirrK [lemma, in mathcomp.character.character]
+conjC_IirrE [lemma, in mathcomp.character.character]
+conjC_Iirr [definition, in mathcomp.character.character]
+conjC_irrAut [lemma, in mathcomp.character.character]
+conjC_charAut [lemma, in mathcomp.character.character]
+conjC_pair_orthogonal [lemma, in mathcomp.character.classfun]
+ConjDef [section, in mathcomp.character.inertia]
+ConjDef.B [variable, in mathcomp.character.inertia]
+ConjDef.gT [variable, in mathcomp.character.inertia]
+ConjDef.phi [variable, in mathcomp.character.inertia]
+ConjDef.y [variable, in mathcomp.character.inertia]
+conjDg [lemma, in mathcomp.fingroup.fingroup]
+conjD1g [lemma, in mathcomp.fingroup.fingroup]
+conjg [definition, in mathcomp.fingroup.fingroup]
+conjgC [lemma, in mathcomp.fingroup.fingroup]
+conjgCV [lemma, in mathcomp.fingroup.fingroup]
+conjgE [lemma, in mathcomp.fingroup.fingroup]
+conjGid [lemma, in mathcomp.fingroup.fingroup]
+conjgK [lemma, in mathcomp.fingroup.fingroup]
+conjgKV [lemma, in mathcomp.fingroup.fingroup]
+conjgm [definition, in mathcomp.fingroup.automorphism]
+conjgM [lemma, in mathcomp.fingroup.fingroup]
+conjgmE [lemma, in mathcomp.fingroup.automorphism]
+conjg_Iirr0 [lemma, in mathcomp.character.inertia]
+conjg_Iirr_eq0 [lemma, in mathcomp.character.inertia]
+conjg_Iirr_inj [lemma, in mathcomp.character.inertia]
+conjg_IirrKV [lemma, in mathcomp.character.inertia]
+conjg_IirrK [lemma, in mathcomp.character.inertia]
+conjg_IirrE [lemma, in mathcomp.character.inertia]
+conjg_Iirr [definition, in mathcomp.character.inertia]
+conjg_inertia [lemma, in mathcomp.character.inertia]
+conjG_action [definition, in mathcomp.fingroup.action]
+conjG_is_action [lemma, in mathcomp.fingroup.action]
+conjg_is_groupAction [lemma, in mathcomp.fingroup.action]
+conjg_Rmul [lemma, in mathcomp.solvable.commutator]
+conjg_mulR [lemma, in mathcomp.solvable.commutator]
+conjg_set1 [lemma, in mathcomp.fingroup.fingroup]
+conjg_preim [lemma, in mathcomp.fingroup.fingroup]
+conjg_fixP [lemma, in mathcomp.fingroup.fingroup]
+conjg_prod [lemma, in mathcomp.fingroup.fingroup]
+conjg_eq1 [lemma, in mathcomp.fingroup.fingroup]
+conjg_inj [lemma, in mathcomp.fingroup.fingroup]
+conjg1 [lemma, in mathcomp.fingroup.fingroup]
+conjIg [lemma, in mathcomp.fingroup.fingroup]
+conjJg [lemma, in mathcomp.fingroup.fingroup]
+conjMg [lemma, in mathcomp.fingroup.fingroup]
+ConjMorph [section, in mathcomp.character.inertia]
+ConjMorph.aT [variable, in mathcomp.character.inertia]
+ConjMorph.D [variable, in mathcomp.character.inertia]
+ConjMorph.eq_hg [variable, in mathcomp.character.inertia]
+ConjMorph.f [variable, in mathcomp.character.inertia]
+ConjMorph.g [variable, in mathcomp.character.inertia]
+ConjMorph.G [variable, in mathcomp.character.inertia]
+ConjMorph.h [variable, in mathcomp.character.inertia]
+ConjMorph.H [variable, in mathcomp.character.inertia]
+ConjMorph.isoG [variable, in mathcomp.character.inertia]
+ConjMorph.isoH [variable, in mathcomp.character.inertia]
+ConjMorph.R [variable, in mathcomp.character.inertia]
+ConjMorph.rT [variable, in mathcomp.character.inertia]
+ConjMorph.S [variable, in mathcomp.character.inertia]
+ConjMorph.sHG [variable, in mathcomp.character.inertia]
+ConjQuotient [section, in mathcomp.character.inertia]
+ConjQuotient.gT [variable, in mathcomp.character.inertia]
+ConjRestrict [section, in mathcomp.character.inertia]
+ConjRestrict.G [variable, in mathcomp.character.inertia]
+ConjRestrict.gT [variable, in mathcomp.character.inertia]
+ConjRestrict.H [variable, in mathcomp.character.inertia]
+ConjRestrict.K [variable, in mathcomp.character.inertia]
+conjRg [lemma, in mathcomp.fingroup.fingroup]
+conjSg [lemma, in mathcomp.fingroup.fingroup]
+conjsgE [lemma, in mathcomp.fingroup.fingroup]
+conjsgK [lemma, in mathcomp.fingroup.fingroup]
+conjsgKV [lemma, in mathcomp.fingroup.fingroup]
+conjsgM [lemma, in mathcomp.fingroup.fingroup]
+conjsg_eq1 [lemma, in mathcomp.fingroup.fingroup]
+conjsg_inj [lemma, in mathcomp.fingroup.fingroup]
+conjsg1 [lemma, in mathcomp.fingroup.fingroup]
+conjsMg [lemma, in mathcomp.fingroup.fingroup]
+conjsRg [lemma, in mathcomp.fingroup.fingroup]
+conjs1g [lemma, in mathcomp.fingroup.fingroup]
+conjTg [lemma, in mathcomp.fingroup.fingroup]
+conjUg [lemma, in mathcomp.fingroup.fingroup]
+conjugate [definition, in mathcomp.fingroup.fingroup]
+conjugates [definition, in mathcomp.fingroup.fingroup]
+conjugatesS [lemma, in mathcomp.fingroup.fingroup]
+conjugates_conj [lemma, in mathcomp.fingroup.fingroup]
+conjugates_set1 [lemma, in mathcomp.fingroup.fingroup]
+ConjugationMorphism [section, in mathcomp.fingroup.automorphism]
+ConjugationMorphism.G [variable, in mathcomp.fingroup.automorphism]
+ConjugationMorphism.gT [variable, in mathcomp.fingroup.automorphism]
+conjVg [lemma, in mathcomp.fingroup.fingroup]
+conjXg [lemma, in mathcomp.fingroup.fingroup]
+conjYg [lemma, in mathcomp.fingroup.fingroup]
+conj_Crat [lemma, in mathcomp.field.algC]
+conj_Cnat [lemma, in mathcomp.field.algC]
+conj_Cint [lemma, in mathcomp.field.algC]
+conj_mx_irr [lemma, in mathcomp.character.mxrepresentation]
+conj_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
+conj_aut_morphM [lemma, in mathcomp.fingroup.automorphism]
+conj_autE [lemma, in mathcomp.fingroup.automorphism]
+conj_aut [definition, in mathcomp.fingroup.automorphism]
+conj_isog [lemma, in mathcomp.fingroup.automorphism]
+conj_isom [lemma, in mathcomp.fingroup.automorphism]
+conj_cfConjg [lemma, in mathcomp.character.inertia]
+conj_astabQ [lemma, in mathcomp.fingroup.action]
+conj_cfInd [definition, in mathcomp.character.classfun]
+conj_cfMod [definition, in mathcomp.character.classfun]
+conj_cfQuo [definition, in mathcomp.character.classfun]
+conj_cfRes [definition, in mathcomp.character.classfun]
+conj_subG [lemma, in mathcomp.fingroup.fingroup]
+Conj.G [variable, in mathcomp.character.inertia]
+Conj.gT [variable, in mathcomp.character.inertia]
+conj0g [lemma, in mathcomp.fingroup.fingroup]
+conj1g [lemma, in mathcomp.fingroup.fingroup]
+connect [definition, in mathcomp.ssreflect.fingraph]
+Connect [section, in mathcomp.ssreflect.fingraph]
+connectP [lemma, in mathcomp.ssreflect.fingraph]
+connect_closed [lemma, in mathcomp.ssreflect.fingraph]
+connect_sub [lemma, in mathcomp.ssreflect.fingraph]
+connect_sym [definition, in mathcomp.ssreflect.fingraph]
+connect_root [lemma, in mathcomp.ssreflect.fingraph]
+connect_trans [lemma, in mathcomp.ssreflect.fingraph]
+Connect.Dfs [section, in mathcomp.ssreflect.fingraph]
+Connect.Dfs.g [variable, in mathcomp.ssreflect.fingraph]
+Connect.e [variable, in mathcomp.ssreflect.fingraph]
+Connect.sym_e [variable, in mathcomp.ssreflect.fingraph]
+Connect.T [variable, in mathcomp.ssreflect.fingraph]
+connect0 [lemma, in mathcomp.ssreflect.fingraph]
+connect1 [lemma, in mathcomp.ssreflect.fingraph]
+Cons [abbreviation, in mathcomp.ssreflect.seq]
+ConsPred [abbreviation, in mathcomp.solvable.pgroup]
+constant [definition, in mathcomp.ssreflect.seq]
+constantP [lemma, in mathcomp.ssreflect.seq]
+constant_nseq [lemma, in mathcomp.ssreflect.seq]
+constt [definition, in mathcomp.solvable.pgroup]
+consttC [lemma, in mathcomp.solvable.pgroup]
+ConsttInertiaBijection [section, in mathcomp.character.inertia]
+ConsttInertiaBijection.calA [variable, in mathcomp.character.inertia]
+ConsttInertiaBijection.calB [variable, in mathcomp.character.inertia]
+ConsttInertiaBijection.G [variable, in mathcomp.character.inertia]
+ConsttInertiaBijection.gT [variable, in mathcomp.character.inertia]
+ConsttInertiaBijection.H [variable, in mathcomp.character.inertia]
+ConsttInertiaBijection.nsHG [variable, in mathcomp.character.inertia]
+ConsttInertiaBijection.t [variable, in mathcomp.character.inertia]
+` T (group_scope) [notation, in mathcomp.character.inertia]
+consttJ [lemma, in mathcomp.solvable.pgroup]
+consttM [lemma, in mathcomp.solvable.pgroup]
+consttNK [lemma, in mathcomp.solvable.pgroup]
+consttV [lemma, in mathcomp.solvable.pgroup]
+consttX [lemma, in mathcomp.solvable.pgroup]
+constt_p_elt [lemma, in mathcomp.solvable.pgroup]
+constt_cfInd_irr [lemma, in mathcomp.character.character]
+constt_cfRes_irr [lemma, in mathcomp.character.character]
+constt_Res_trans [lemma, in mathcomp.character.character]
+constt_Ind_Res [lemma, in mathcomp.character.character]
+constt_ortho_char [lemma, in mathcomp.character.character]
+constt_irr [lemma, in mathcomp.character.character]
+constt_charP [lemma, in mathcomp.character.character]
+constt_Ind_ext [lemma, in mathcomp.character.inertia]
+constt_Ind_mul_ext [lemma, in mathcomp.character.inertia]
+constt_Inertia_bijection [lemma, in mathcomp.character.inertia]
+constt0_Res_cfker [lemma, in mathcomp.character.inertia]
+constt1 [lemma, in mathcomp.solvable.pgroup]
+constt1P [lemma, in mathcomp.solvable.pgroup]
+const_mx_is_additive [lemma, in mathcomp.algebra.matrix]
+const_mx [definition, in mathcomp.algebra.matrix]
+const_mx_key [lemma, in mathcomp.algebra.matrix]
+cons_pfactor [definition, in mathcomp.ssreflect.prime]
+cons_uniq [lemma, in mathcomp.ssreflect.seq]
+cons_poly_def [lemma, in mathcomp.algebra.poly]
+cons_poly [definition, in mathcomp.algebra.poly]
+contraFeq [lemma, in mathcomp.ssreflect.eqtype]
+contraFneq [lemma, in mathcomp.ssreflect.eqtype]
+contraNeq [lemma, in mathcomp.ssreflect.eqtype]
+contraNneq [lemma, in mathcomp.ssreflect.eqtype]
+Contrapositives [section, in mathcomp.ssreflect.eqtype]
+Contrapositives.T1 [variable, in mathcomp.ssreflect.eqtype]
+Contrapositives.T2 [variable, in mathcomp.ssreflect.eqtype]
+contraTeq [lemma, in mathcomp.ssreflect.eqtype]
+contraTneq [lemma, in mathcomp.ssreflect.eqtype]
+contra_orbit [lemma, in mathcomp.fingroup.action]
+contra_neq [lemma, in mathcomp.ssreflect.eqtype]
+contra_eq [lemma, in mathcomp.ssreflect.eqtype]
+contra_eqT [lemma, in mathcomp.ssreflect.eqtype]
+contra_eqF [lemma, in mathcomp.ssreflect.eqtype]
+contra_eqN [lemma, in mathcomp.ssreflect.eqtype]
+coord [definition, in mathcomp.algebra.vector]
+coord_vbasis [lemma, in mathcomp.algebra.vector]
+coord_basis [lemma, in mathcomp.algebra.vector]
+coord_sum_free [lemma, in mathcomp.algebra.vector]
+coord_free [lemma, in mathcomp.algebra.vector]
+coord_span [lemma, in mathcomp.algebra.vector]
+coord_is_scalar [lemma, in mathcomp.algebra.vector]
+coord_expanded_def [definition, in mathcomp.algebra.vector]
+coord_cfdot [lemma, in mathcomp.character.character]
+coord0 [lemma, in mathcomp.algebra.vector]
+copid_mx_id [lemma, in mathcomp.algebra.matrix]
+copid_mx [definition, in mathcomp.algebra.matrix]
+coprime [definition, in mathcomp.ssreflect.div]
+coprimegS [lemma, in mathcomp.fingroup.fingroup]
+coprimenP [lemma, in mathcomp.ssreflect.div]
+coprimenS [lemma, in mathcomp.ssreflect.div]
+coprimeNz [lemma, in mathcomp.algebra.intdiv]
+coprimen1 [lemma, in mathcomp.ssreflect.div]
+coprimen2 [lemma, in mathcomp.ssreflect.div]
+coprimeP [lemma, in mathcomp.ssreflect.div]
+coprimePn [lemma, in mathcomp.ssreflect.div]
+coprimeq_den [lemma, in mathcomp.algebra.rat]
+coprimeq_num [lemma, in mathcomp.algebra.rat]
+coprimeSg [lemma, in mathcomp.fingroup.fingroup]
+coprimeSn [lemma, in mathcomp.ssreflect.div]
+coprimez [definition, in mathcomp.algebra.intdiv]
+coprimezE [lemma, in mathcomp.algebra.intdiv]
+coprimezN [lemma, in mathcomp.algebra.intdiv]
+coprimezP [lemma, in mathcomp.algebra.intdiv]
+coprimez_dvdr [lemma, in mathcomp.algebra.intdiv]
+coprimez_dvdl [lemma, in mathcomp.algebra.intdiv]
+coprimez_expr [lemma, in mathcomp.algebra.intdiv]
+coprimez_expl [lemma, in mathcomp.algebra.intdiv]
+coprimez_pexpr [lemma, in mathcomp.algebra.intdiv]
+coprimez_pexpl [lemma, in mathcomp.algebra.intdiv]
+coprimez_mull [lemma, in mathcomp.algebra.intdiv]
+coprimez_mulr [lemma, in mathcomp.algebra.intdiv]
+coprimez_sym [lemma, in mathcomp.algebra.intdiv]
+coprime_degree_support_cfcenter [lemma, in mathcomp.character.integral_char]
+coprime_num_den [lemma, in mathcomp.algebra.rat]
+coprime_Hall_subset [lemma, in mathcomp.solvable.hall]
+coprime_comm_pcore [lemma, in mathcomp.solvable.hall]
+coprime_quotient_cent [lemma, in mathcomp.solvable.hall]
+coprime_cent_mulG [lemma, in mathcomp.solvable.hall]
+coprime_norm_quotient_cent [lemma, in mathcomp.solvable.hall]
+coprime_Hall_trans [lemma, in mathcomp.solvable.hall]
+coprime_Hall_exists [lemma, in mathcomp.solvable.hall]
+coprime_norm_cent [lemma, in mathcomp.solvable.hall]
+coprime_pcoreC [lemma, in mathcomp.solvable.pgroup]
+coprime_sdprod_Hall_r [lemma, in mathcomp.solvable.pgroup]
+coprime_sdprod_Hall_l [lemma, in mathcomp.solvable.pgroup]
+coprime_mulGp_Hall [lemma, in mathcomp.solvable.pgroup]
+coprime_mulpG_Hall [lemma, in mathcomp.solvable.pgroup]
+coprime_p'group [lemma, in mathcomp.solvable.pgroup]
+coprime_morph [lemma, in mathcomp.fingroup.quotient]
+coprime_morphr [lemma, in mathcomp.fingroup.quotient]
+coprime_morphl [lemma, in mathcomp.fingroup.quotient]
+coprime_partC [lemma, in mathcomp.ssreflect.prime]
+coprime_pi' [lemma, in mathcomp.ssreflect.prime]
+coprime_has_primes [lemma, in mathcomp.ssreflect.prime]
+coprime_egcdn [lemma, in mathcomp.ssreflect.div]
+coprime_dvdr [lemma, in mathcomp.ssreflect.div]
+coprime_dvdl [lemma, in mathcomp.ssreflect.div]
+coprime_expr [lemma, in mathcomp.ssreflect.div]
+coprime_expl [lemma, in mathcomp.ssreflect.div]
+coprime_pexpr [lemma, in mathcomp.ssreflect.div]
+coprime_pexpl [lemma, in mathcomp.ssreflect.div]
+coprime_mull [lemma, in mathcomp.ssreflect.div]
+coprime_mulr [lemma, in mathcomp.ssreflect.div]
+coprime_modr [lemma, in mathcomp.ssreflect.div]
+coprime_modl [lemma, in mathcomp.ssreflect.div]
+coprime_sym [lemma, in mathcomp.ssreflect.div]
+coprime_abel_cent_TI [lemma, in mathcomp.solvable.finmodule]
+coprime_index_mulG [lemma, in mathcomp.fingroup.fingroup]
+coprime_cardMg [lemma, in mathcomp.fingroup.fingroup]
+coprime_TIg [lemma, in mathcomp.fingroup.fingroup]
+coprime_mulG_setI_norm [lemma, in mathcomp.solvable.sylow]
+coprime1n [lemma, in mathcomp.ssreflect.div]
+coprime2n [lemma, in mathcomp.ssreflect.div]
+CormenLUP [section, in mathcomp.algebra.matrix]
+CormenLUP.F [variable, in mathcomp.algebra.matrix]
+cormen_lup_upper [lemma, in mathcomp.algebra.matrix]
+cormen_lup_lower [lemma, in mathcomp.algebra.matrix]
+cormen_lup_detL [lemma, in mathcomp.algebra.matrix]
+cormen_lup_correct [lemma, in mathcomp.algebra.matrix]
+cormen_lup_perm [lemma, in mathcomp.algebra.matrix]
+cormen_lup [definition, in mathcomp.algebra.matrix]
+coset [definition, in mathcomp.fingroup.quotient]
+Coset [constructor, in mathcomp.fingroup.quotient]
+Coset [section, in mathcomp.character.character]
+Coset [section, in mathcomp.character.classfun]
+CosetOfGroupTheory [section, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.gT [variable, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.H [variable, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.Injective [section, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.Injective.G [variable, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.Injective.nHG [variable, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.Injective.tiHG [variable, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.InverseImage [section, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.InverseImage.G [variable, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.InverseImage.Kbar [variable, in mathcomp.fingroup.quotient]
+CosetOfGroupTheory.InverseImage.nHG [variable, in mathcomp.fingroup.quotient]
+_ / _ (Group_scope) [notation, in mathcomp.fingroup.quotient]
+cosetP [lemma, in mathcomp.fingroup.quotient]
+cosetpreK [lemma, in mathcomp.fingroup.quotient]
+cosetpreM [lemma, in mathcomp.fingroup.quotient]
+cosetpreSK [lemma, in mathcomp.fingroup.quotient]
+cosetpre_subcent [lemma, in mathcomp.fingroup.quotient]
+cosetpre_cents [lemma, in mathcomp.fingroup.quotient]
+cosetpre_cent [lemma, in mathcomp.fingroup.quotient]
+cosetpre_subcent1 [lemma, in mathcomp.fingroup.quotient]
+cosetpre_cent1s [lemma, in mathcomp.fingroup.quotient]
+cosetpre_cent1 [lemma, in mathcomp.fingroup.quotient]
+cosetpre_normal [lemma, in mathcomp.fingroup.quotient]
+cosetpre_gen [lemma, in mathcomp.fingroup.quotient]
+cosetpre_set1_coset [lemma, in mathcomp.fingroup.quotient]
+cosetpre_set1 [lemma, in mathcomp.fingroup.quotient]
+cosetpre_proper [lemma, in mathcomp.fingroup.quotient]
+cosetpre_maximal_eq [lemma, in mathcomp.solvable.gseries]
+cosetpre_maximal [lemma, in mathcomp.solvable.gseries]
+cosetpre1 [lemma, in mathcomp.fingroup.quotient]
+Cosets [section, in mathcomp.fingroup.quotient]
+Cosets.A [variable, in mathcomp.fingroup.quotient]
+Cosets.gT [variable, in mathcomp.fingroup.quotient]
+Cosets.nNH [variable, in mathcomp.fingroup.quotient]
+Cosets.Q [variable, in mathcomp.fingroup.quotient]
+coset_kerr [lemma, in mathcomp.fingroup.quotient]
+coset_kerl [lemma, in mathcomp.fingroup.quotient]
+coset_idr [lemma, in mathcomp.fingroup.quotient]
+coset_norm [lemma, in mathcomp.fingroup.quotient]
+coset_default [lemma, in mathcomp.fingroup.quotient]
+coset_id [lemma, in mathcomp.fingroup.quotient]
+coset_reprK [lemma, in mathcomp.fingroup.quotient]
+coset_mem [lemma, in mathcomp.fingroup.quotient]
+coset_morphM [lemma, in mathcomp.fingroup.quotient]
+coset_of_groupMixin [definition, in mathcomp.fingroup.quotient]
+coset_invP [lemma, in mathcomp.fingroup.quotient]
+coset_oneP [lemma, in mathcomp.fingroup.quotient]
+coset_mulP [lemma, in mathcomp.fingroup.quotient]
+coset_inv [definition, in mathcomp.fingroup.quotient]
+coset_range_inv [lemma, in mathcomp.fingroup.quotient]
+coset_mul [definition, in mathcomp.fingroup.quotient]
+coset_range_mul [lemma, in mathcomp.fingroup.quotient]
+coset_one [definition, in mathcomp.fingroup.quotient]
+coset_one_proof [lemma, in mathcomp.fingroup.quotient]
+coset_finMixin [definition, in mathcomp.fingroup.quotient]
+coset_countMixin [definition, in mathcomp.fingroup.quotient]
+coset_choiceMixin [definition, in mathcomp.fingroup.quotient]
+coset_eqMixin [definition, in mathcomp.fingroup.quotient]
+coset_of [record, in mathcomp.fingroup.quotient]
+coset_range [definition, in mathcomp.fingroup.quotient]
+coset_splitting_field [lemma, in mathcomp.character.mxrepresentation]
+Coset.B [variable, in mathcomp.character.classfun]
+Coset.G [variable, in mathcomp.character.classfun]
+Coset.gT [variable, in mathcomp.character.character]
+Coset.gT [variable, in mathcomp.character.classfun]
+_ %% B (cfun_scope) [notation, in mathcomp.character.classfun]
+_ / B (cfun_scope) [notation, in mathcomp.character.classfun]
+coset1 [lemma, in mathcomp.fingroup.quotient]
+coset1_injm [lemma, in mathcomp.fingroup.quotient]
+count [definition, in mathcomp.ssreflect.seq]
+Countable [module, in mathcomp.ssreflect.choice]
+CountableDataTypes [section, in mathcomp.ssreflect.choice]
+CountableTheory [section, in mathcomp.ssreflect.choice]
+CountableTheory.T [variable, in mathcomp.ssreflect.choice]
+countable_algebraic_closure [lemma, in mathcomp.field.countalg]
+countable_field_extension [lemma, in mathcomp.field.countalg]
+Countable.base [projection, in mathcomp.ssreflect.choice]
+Countable.ChoiceMixin [definition, in mathcomp.ssreflect.choice]
+Countable.choiceType [definition, in mathcomp.ssreflect.choice]
+Countable.class [definition, in mathcomp.ssreflect.choice]
+Countable.Class [constructor, in mathcomp.ssreflect.choice]
+Countable.ClassDef [section, in mathcomp.ssreflect.choice]
+Countable.ClassDef.cT [variable, in mathcomp.ssreflect.choice]
+Countable.ClassDef.T [variable, in mathcomp.ssreflect.choice]
+Countable.ClassDef.xT [variable, in mathcomp.ssreflect.choice]
+Countable.class_of [record, in mathcomp.ssreflect.choice]
+Countable.clone [definition, in mathcomp.ssreflect.choice]
+Countable.EqMixin [definition, in mathcomp.ssreflect.choice]
+Countable.eqType [definition, in mathcomp.ssreflect.choice]
+Countable.Exports [module, in mathcomp.ssreflect.choice]
+Countable.Exports.CountChoiceMixin [abbreviation, in mathcomp.ssreflect.choice]
+Countable.Exports.CountMixin [abbreviation, in mathcomp.ssreflect.choice]
+Countable.Exports.CountType [abbreviation, in mathcomp.ssreflect.choice]
+Countable.Exports.countType [abbreviation, in mathcomp.ssreflect.choice]
+[ countType of _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
+[ countType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.choice]
+Countable.mixin [projection, in mathcomp.ssreflect.choice]
+Countable.Mixin [constructor, in mathcomp.ssreflect.choice]
+Countable.mixin_of [record, in mathcomp.ssreflect.choice]
+Countable.pack [definition, in mathcomp.ssreflect.choice]
+Countable.Pack [constructor, in mathcomp.ssreflect.choice]
+Countable.pickle [projection, in mathcomp.ssreflect.choice]
+Countable.pickleK [projection, in mathcomp.ssreflect.choice]
+Countable.sort [projection, in mathcomp.ssreflect.choice]
+Countable.type [record, in mathcomp.ssreflect.choice]
+Countable.unpickle [projection, in mathcomp.ssreflect.choice]
+Countable.xclass [abbreviation, in mathcomp.ssreflect.choice]
+countalg [library]
+CountEncodingModuloRel [section, in mathcomp.ssreflect.generic_quotient]
+CountEncodingModuloRel.C [variable, in mathcomp.ssreflect.generic_quotient]
+CountEncodingModuloRel.CD [variable, in mathcomp.ssreflect.generic_quotient]
+CountEncodingModuloRel.D [variable, in mathcomp.ssreflect.generic_quotient]
+CountEncodingModuloRel.DC [variable, in mathcomp.ssreflect.generic_quotient]
+CountEncodingModuloRel.eD [variable, in mathcomp.ssreflect.generic_quotient]
+CountEncodingModuloRel.encD [variable, in mathcomp.ssreflect.generic_quotient]
+CountRing [module, in mathcomp.field.countalg]
+CountRing.ClosedField [module, in mathcomp.field.countalg]
+CountRing.ClosedField.base [projection, in mathcomp.field.countalg]
+CountRing.ClosedField.base2 [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.choiceType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.class [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.Class [constructor, in mathcomp.field.countalg]
+CountRing.ClosedField.ClassDef [section, in mathcomp.field.countalg]
+CountRing.ClosedField.ClassDef.cT [variable, in mathcomp.field.countalg]
+CountRing.ClosedField.ClassDef.xT [variable, in mathcomp.field.countalg]
+CountRing.ClosedField.class_of [record, in mathcomp.field.countalg]
+CountRing.ClosedField.closedFieldType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.comRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.comUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.countComRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.countComUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.countDecFieldType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.countFieldType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.countIdomainType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.countRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.countType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.countZmodType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.decFieldType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.eqType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.Exports [module, in mathcomp.field.countalg]
+CountRing.ClosedField.Exports.countClosedFieldType [abbreviation, in mathcomp.field.countalg]
+[ countClosedFieldType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
+CountRing.ClosedField.fieldType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.idomainType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.join_countDecFieldType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.join_countFieldType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.join_countIdomainType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.join_countComUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.join_countComRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.join_countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.join_countRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.join_countZmodType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.join_countType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.mixin [projection, in mathcomp.field.countalg]
+CountRing.ClosedField.pack [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.Pack [constructor, in mathcomp.field.countalg]
+CountRing.ClosedField.ringType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.sort [projection, in mathcomp.field.countalg]
+CountRing.ClosedField.type [record, in mathcomp.field.countalg]
+CountRing.ClosedField.unitRingType [definition, in mathcomp.field.countalg]
+CountRing.ClosedField.xclass [abbreviation, in mathcomp.field.countalg]
+CountRing.ClosedField.zmodType [definition, in mathcomp.field.countalg]
+CountRing.cnt_ [abbreviation, in mathcomp.field.countalg]
+CountRing.ComRing [module, in mathcomp.field.countalg]
+CountRing.ComRing.base [projection, in mathcomp.field.countalg]
+CountRing.ComRing.base2 [definition, in mathcomp.field.countalg]
+CountRing.ComRing.choiceType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.class [definition, in mathcomp.field.countalg]
+CountRing.ComRing.Class [constructor, in mathcomp.field.countalg]
+CountRing.ComRing.ClassDef [section, in mathcomp.field.countalg]
+CountRing.ComRing.ClassDef.cT [variable, in mathcomp.field.countalg]
+CountRing.ComRing.ClassDef.xT [variable, in mathcomp.field.countalg]
+CountRing.ComRing.class_of [record, in mathcomp.field.countalg]
+CountRing.ComRing.comRingType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.countRingType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.countType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.countZmodType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.eqType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.Exports [module, in mathcomp.field.countalg]
+CountRing.ComRing.Exports.countComRingType [abbreviation, in mathcomp.field.countalg]
+[ countComRingType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
+CountRing.ComRing.join_countRingType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.join_countZmodType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.join_countType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.mixin [projection, in mathcomp.field.countalg]
+CountRing.ComRing.pack [definition, in mathcomp.field.countalg]
+CountRing.ComRing.Pack [constructor, in mathcomp.field.countalg]
+CountRing.ComRing.ringType [definition, in mathcomp.field.countalg]
+CountRing.ComRing.sort [projection, in mathcomp.field.countalg]
+CountRing.ComRing.type [record, in mathcomp.field.countalg]
+CountRing.ComRing.xclass [abbreviation, in mathcomp.field.countalg]
+CountRing.ComRing.zmodType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing [module, in mathcomp.field.countalg]
+CountRing.ComUnitRing.base [projection, in mathcomp.field.countalg]
+CountRing.ComUnitRing.base2 [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.base3 [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.ccjoin_countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.choiceType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.cjoin_countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.class [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.Class [constructor, in mathcomp.field.countalg]
+CountRing.ComUnitRing.ClassDef [section, in mathcomp.field.countalg]
+CountRing.ComUnitRing.ClassDef.cT [variable, in mathcomp.field.countalg]
+CountRing.ComUnitRing.ClassDef.xT [variable, in mathcomp.field.countalg]
+CountRing.ComUnitRing.class_of [record, in mathcomp.field.countalg]
+CountRing.ComUnitRing.comRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.comUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.countComRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.countRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.countType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.countZmodType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.eqType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.Exports [module, in mathcomp.field.countalg]
+CountRing.ComUnitRing.Exports.countComUnitRingType [abbreviation, in mathcomp.field.countalg]
+[ countComUnitRingType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
+CountRing.ComUnitRing.join_countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.join_countComRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.join_countRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.join_countZmodType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.join_countType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.mixin [projection, in mathcomp.field.countalg]
+CountRing.ComUnitRing.pack [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.Pack [constructor, in mathcomp.field.countalg]
+CountRing.ComUnitRing.ringType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.sort [projection, in mathcomp.field.countalg]
+CountRing.ComUnitRing.type [record, in mathcomp.field.countalg]
+CountRing.ComUnitRing.ujoin_countComRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.unitRingType [definition, in mathcomp.field.countalg]
+CountRing.ComUnitRing.xclass [abbreviation, in mathcomp.field.countalg]
+CountRing.ComUnitRing.zmodType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField [module, in mathcomp.field.countalg]
+CountRing.DecidableField.base [projection, in mathcomp.field.countalg]
+CountRing.DecidableField.base2 [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.choiceType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.class [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.Class [constructor, in mathcomp.field.countalg]
+CountRing.DecidableField.ClassDef [section, in mathcomp.field.countalg]
+CountRing.DecidableField.ClassDef.cT [variable, in mathcomp.field.countalg]
+CountRing.DecidableField.ClassDef.xT [variable, in mathcomp.field.countalg]
+CountRing.DecidableField.class_of [record, in mathcomp.field.countalg]
+CountRing.DecidableField.comRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.comUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.countComRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.countComUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.countFieldType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.countIdomainType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.countRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.countType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.countZmodType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.decFieldType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.eqType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.Exports [module, in mathcomp.field.countalg]
+CountRing.DecidableField.Exports.countDecFieldType [abbreviation, in mathcomp.field.countalg]
+[ countDecFieldType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
+CountRing.DecidableField.fieldType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.idomainType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.join_countFieldType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.join_countIdomainType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.join_countComUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.join_countComRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.join_countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.join_countRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.join_countZmodType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.join_countType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.mixin [projection, in mathcomp.field.countalg]
+CountRing.DecidableField.pack [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.Pack [constructor, in mathcomp.field.countalg]
+CountRing.DecidableField.ringType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.sort [projection, in mathcomp.field.countalg]
+CountRing.DecidableField.type [record, in mathcomp.field.countalg]
+CountRing.DecidableField.unitRingType [definition, in mathcomp.field.countalg]
+CountRing.DecidableField.xclass [abbreviation, in mathcomp.field.countalg]
+CountRing.DecidableField.zmodType [definition, in mathcomp.field.countalg]
+CountRing.do_pack [abbreviation, in mathcomp.field.countalg]
+CountRing.Field [module, in mathcomp.field.countalg]
+CountRing.Field.base [projection, in mathcomp.field.countalg]
+CountRing.Field.base2 [definition, in mathcomp.field.countalg]
+CountRing.Field.choiceType [definition, in mathcomp.field.countalg]
+CountRing.Field.class [definition, in mathcomp.field.countalg]
+CountRing.Field.Class [constructor, in mathcomp.field.countalg]
+CountRing.Field.ClassDef [section, in mathcomp.field.countalg]
+CountRing.Field.ClassDef.cT [variable, in mathcomp.field.countalg]
+CountRing.Field.ClassDef.xT [variable, in mathcomp.field.countalg]
+CountRing.Field.class_of [record, in mathcomp.field.countalg]
+CountRing.Field.comRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.comUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.countComRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.countComUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.countIdomainType [definition, in mathcomp.field.countalg]
+CountRing.Field.countRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.countType [definition, in mathcomp.field.countalg]
+CountRing.Field.countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.countZmodType [definition, in mathcomp.field.countalg]
+CountRing.Field.eqType [definition, in mathcomp.field.countalg]
+CountRing.Field.Exports [module, in mathcomp.field.countalg]
+CountRing.Field.Exports.countFieldType [abbreviation, in mathcomp.field.countalg]
+[ countFieldType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
+CountRing.Field.fieldType [definition, in mathcomp.field.countalg]
+CountRing.Field.idomainType [definition, in mathcomp.field.countalg]
+CountRing.Field.join_countIdomainType [definition, in mathcomp.field.countalg]
+CountRing.Field.join_countComUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.join_countComRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.join_countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.join_countRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.join_countZmodType [definition, in mathcomp.field.countalg]
+CountRing.Field.join_countType [definition, in mathcomp.field.countalg]
+CountRing.Field.mixin [projection, in mathcomp.field.countalg]
+CountRing.Field.pack [definition, in mathcomp.field.countalg]
+CountRing.Field.Pack [constructor, in mathcomp.field.countalg]
+CountRing.Field.ringType [definition, in mathcomp.field.countalg]
+CountRing.Field.sort [projection, in mathcomp.field.countalg]
+CountRing.Field.type [record, in mathcomp.field.countalg]
+CountRing.Field.unitRingType [definition, in mathcomp.field.countalg]
+CountRing.Field.xclass [abbreviation, in mathcomp.field.countalg]
+CountRing.Field.zmodType [definition, in mathcomp.field.countalg]
+CountRing.Generic [section, in mathcomp.field.countalg]
+CountRing.Generic.base_class [variable, in mathcomp.field.countalg]
+CountRing.Generic.base_sort [variable, in mathcomp.field.countalg]
+CountRing.Generic.base_of [variable, in mathcomp.field.countalg]
+CountRing.Generic.base_type [variable, in mathcomp.field.countalg]
+CountRing.Generic.Class [variable, in mathcomp.field.countalg]
+CountRing.Generic.class_of [variable, in mathcomp.field.countalg]
+CountRing.Generic.Pack [variable, in mathcomp.field.countalg]
+CountRing.Generic.type [variable, in mathcomp.field.countalg]
+CountRing.gen_pack [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain [module, in mathcomp.field.countalg]
+CountRing.IntegralDomain.base [projection, in mathcomp.field.countalg]
+CountRing.IntegralDomain.base2 [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.choiceType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.class [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.Class [constructor, in mathcomp.field.countalg]
+CountRing.IntegralDomain.ClassDef [section, in mathcomp.field.countalg]
+CountRing.IntegralDomain.ClassDef.cT [variable, in mathcomp.field.countalg]
+CountRing.IntegralDomain.ClassDef.xT [variable, in mathcomp.field.countalg]
+CountRing.IntegralDomain.class_of [record, in mathcomp.field.countalg]
+CountRing.IntegralDomain.comRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.comUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.countComRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.countComUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.countRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.countType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.countZmodType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.eqType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.Exports [module, in mathcomp.field.countalg]
+CountRing.IntegralDomain.Exports.countIdomainType [abbreviation, in mathcomp.field.countalg]
+[ countIdomainType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
+CountRing.IntegralDomain.idomainType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.join_countComUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.join_countComRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.join_countUnitRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.join_countRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.join_countZmodType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.join_countType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.mixin [projection, in mathcomp.field.countalg]
+CountRing.IntegralDomain.pack [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.Pack [constructor, in mathcomp.field.countalg]
+CountRing.IntegralDomain.ringType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.sort [projection, in mathcomp.field.countalg]
+CountRing.IntegralDomain.type [record, in mathcomp.field.countalg]
+CountRing.IntegralDomain.unitRingType [definition, in mathcomp.field.countalg]
+CountRing.IntegralDomain.xclass [abbreviation, in mathcomp.field.countalg]
+CountRing.IntegralDomain.zmodType [definition, in mathcomp.field.countalg]
+CountRing.mixin_of [abbreviation, in mathcomp.field.countalg]
+CountRing.Ring [module, in mathcomp.field.countalg]
+CountRing.Ring.base [projection, in mathcomp.field.countalg]
+CountRing.Ring.base2 [definition, in mathcomp.field.countalg]
+CountRing.Ring.choiceType [definition, in mathcomp.field.countalg]
+CountRing.Ring.class [definition, in mathcomp.field.countalg]
+CountRing.Ring.Class [constructor, in mathcomp.field.countalg]
+CountRing.Ring.ClassDef [section, in mathcomp.field.countalg]
+CountRing.Ring.ClassDef.cT [variable, in mathcomp.field.countalg]
+CountRing.Ring.ClassDef.xT [variable, in mathcomp.field.countalg]
+CountRing.Ring.class_of [record, in mathcomp.field.countalg]
+CountRing.Ring.countType [definition, in mathcomp.field.countalg]
+CountRing.Ring.countZmodType [definition, in mathcomp.field.countalg]
+CountRing.Ring.eqType [definition, in mathcomp.field.countalg]
+CountRing.Ring.Exports [module, in mathcomp.field.countalg]
+CountRing.Ring.Exports.countRingType [abbreviation, in mathcomp.field.countalg]
+[ countRingType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
+CountRing.Ring.join_countZmodType [definition, in mathcomp.field.countalg]
+CountRing.Ring.join_countType [definition, in mathcomp.field.countalg]
+CountRing.Ring.mixin [projection, in mathcomp.field.countalg]
+CountRing.Ring.pack [definition, in mathcomp.field.countalg]
+CountRing.Ring.Pack [constructor, in mathcomp.field.countalg]
+CountRing.Ring.ringType [definition, in mathcomp.field.countalg]
+CountRing.Ring.sort [projection, in mathcomp.field.countalg]
+CountRing.Ring.type [record, in mathcomp.field.countalg]
+CountRing.Ring.xclass [abbreviation, in mathcomp.field.countalg]
+CountRing.Ring.zmodType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing [module, in mathcomp.field.countalg]
+CountRing.UnitRing.base [projection, in mathcomp.field.countalg]
+CountRing.UnitRing.base2 [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.choiceType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.class [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.Class [constructor, in mathcomp.field.countalg]
+CountRing.UnitRing.ClassDef [section, in mathcomp.field.countalg]
+CountRing.UnitRing.ClassDef.cT [variable, in mathcomp.field.countalg]
+CountRing.UnitRing.ClassDef.xT [variable, in mathcomp.field.countalg]
+CountRing.UnitRing.class_of [record, in mathcomp.field.countalg]
+CountRing.UnitRing.countRingType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.countType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.countZmodType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.eqType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.Exports [module, in mathcomp.field.countalg]
+CountRing.UnitRing.Exports.countUnitRingType [abbreviation, in mathcomp.field.countalg]
+[ countUnitRingType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
+CountRing.UnitRing.join_countRingType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.join_countZmodType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.join_countType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.mixin [projection, in mathcomp.field.countalg]
+CountRing.UnitRing.pack [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.Pack [constructor, in mathcomp.field.countalg]
+CountRing.UnitRing.ringType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.sort [projection, in mathcomp.field.countalg]
+CountRing.UnitRing.type [record, in mathcomp.field.countalg]
+CountRing.UnitRing.unitRingType [definition, in mathcomp.field.countalg]
+CountRing.UnitRing.xclass [abbreviation, in mathcomp.field.countalg]
+CountRing.UnitRing.zmodType [definition, in mathcomp.field.countalg]
+CountRing.Zmodule [module, in mathcomp.field.countalg]
+CountRing.Zmodule.base [projection, in mathcomp.field.countalg]
+CountRing.Zmodule.choiceType [definition, in mathcomp.field.countalg]
+CountRing.Zmodule.class [definition, in mathcomp.field.countalg]
+CountRing.Zmodule.Class [constructor, in mathcomp.field.countalg]
+CountRing.Zmodule.ClassDef [section, in mathcomp.field.countalg]
+CountRing.Zmodule.ClassDef.cT [variable, in mathcomp.field.countalg]
+CountRing.Zmodule.ClassDef.xT [variable, in mathcomp.field.countalg]
+CountRing.Zmodule.class_of [record, in mathcomp.field.countalg]
+CountRing.Zmodule.countType [definition, in mathcomp.field.countalg]
+CountRing.Zmodule.eqType [definition, in mathcomp.field.countalg]
+CountRing.Zmodule.Exports [module, in mathcomp.field.countalg]
+CountRing.Zmodule.Exports.countZmodType [abbreviation, in mathcomp.field.countalg]
+[ countZmodType of _ ] (form_scope) [notation, in mathcomp.field.countalg]
+CountRing.Zmodule.join_countType [definition, in mathcomp.field.countalg]
+CountRing.Zmodule.mixin [projection, in mathcomp.field.countalg]
+CountRing.Zmodule.pack [definition, in mathcomp.field.countalg]
+CountRing.Zmodule.Pack [constructor, in mathcomp.field.countalg]
+CountRing.Zmodule.sort [projection, in mathcomp.field.countalg]
+CountRing.Zmodule.type [record, in mathcomp.field.countalg]
+CountRing.Zmodule.xclass [abbreviation, in mathcomp.field.countalg]
+CountRing.Zmodule.zmodType [definition, in mathcomp.field.countalg]
+count_flatten [lemma, in mathcomp.ssreflect.seq]
+count_map [lemma, in mathcomp.ssreflect.seq]
+count_mem_uniq [lemma, in mathcomp.ssreflect.seq]
+count_uniq_mem [lemma, in mathcomp.ssreflect.seq]
+count_memPn [lemma, in mathcomp.ssreflect.seq]
+count_rev [lemma, in mathcomp.ssreflect.seq]
+count_mem [abbreviation, in mathcomp.ssreflect.seq]
+count_filter [lemma, in mathcomp.ssreflect.seq]
+count_predC [lemma, in mathcomp.ssreflect.seq]
+count_predUI [lemma, in mathcomp.ssreflect.seq]
+count_predT [lemma, in mathcomp.ssreflect.seq]
+count_pred0 [lemma, in mathcomp.ssreflect.seq]
+count_cat [lemma, in mathcomp.ssreflect.seq]
+count_size [lemma, in mathcomp.ssreflect.seq]
+count_logn_dprod_cycle [lemma, in mathcomp.solvable.abelian]
+cover [definition, in mathcomp.ssreflect.finset]
+cover_partition [lemma, in mathcomp.ssreflect.finset]
+cover_imset [lemma, in mathcomp.ssreflect.finset]
+cover_setI [lemma, in mathcomp.ssreflect.finset]
+cpairg1 [definition, in mathcomp.solvable.center]
+cpairg1_center [lemma, in mathcomp.solvable.center]
+cpairg1_dom [lemma, in mathcomp.solvable.center]
+cpair_center_id [lemma, in mathcomp.solvable.center]
+cpair1g [definition, in mathcomp.solvable.center]
+cpair1g_center [lemma, in mathcomp.solvable.center]
+cpair1g_dom [lemma, in mathcomp.solvable.center]
+cprod [abbreviation, in mathcomp.fingroup.gproduct]
+cprod [abbreviation, in mathcomp.fingroup.gproduct]
+cprodA [lemma, in mathcomp.fingroup.gproduct]
+CprodBy [section, in mathcomp.solvable.center]
+CprodBy.ExtCprodm [section, in mathcomp.solvable.center]
+CprodBy.ExtCprodm.cfHK [variable, in mathcomp.solvable.center]
+CprodBy.ExtCprodm.eq_fHK [variable, in mathcomp.solvable.center]
+CprodBy.ExtCprodm.fH [variable, in mathcomp.solvable.center]
+CprodBy.ExtCprodm.fK [variable, in mathcomp.solvable.center]
+CprodBy.ExtCprodm.gH [variable, in mathcomp.solvable.center]
+CprodBy.ExtCprodm.gK [variable, in mathcomp.solvable.center]
+CprodBy.ExtCprodm.rT [variable, in mathcomp.solvable.center]
+CprodBy.gTH [variable, in mathcomp.solvable.center]
+CprodBy.gTK [variable, in mathcomp.solvable.center]
+CprodBy.gz [variable, in mathcomp.solvable.center]
+CprodBy.gzZ [variable, in mathcomp.solvable.center]
+CprodBy.gzZchar [variable, in mathcomp.solvable.center]
+CprodBy.H [variable, in mathcomp.solvable.center]
+CprodBy.injgz [variable, in mathcomp.solvable.center]
+CprodBy.injH [variable, in mathcomp.solvable.center]
+CprodBy.injK [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism [section, in mathcomp.solvable.center]
+CprodBy.Isomorphism.AutZHfull [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism.defG [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism.G [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism.GH [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism.GK [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism.gzZ_lone [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism.isoGH [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism.isoGK [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism.rT [variable, in mathcomp.solvable.center]
+CprodBy.Isomorphism.ziGHK [variable, in mathcomp.solvable.center]
+CprodBy.isoZ [variable, in mathcomp.solvable.center]
+CprodBy.K [variable, in mathcomp.solvable.center]
+CprodBy.kerHK [variable, in mathcomp.solvable.center]
+CprodBy.sgzZG [variable, in mathcomp.solvable.center]
+CprodBy.sgzZZ [variable, in mathcomp.solvable.center]
+CprodBy.sZH [variable, in mathcomp.solvable.center]
+CprodBy.sZK [variable, in mathcomp.solvable.center]
+cprodC [lemma, in mathcomp.fingroup.gproduct]
+cprodE [lemma, in mathcomp.fingroup.gproduct]
+cprodEY [lemma, in mathcomp.fingroup.gproduct]
+cprodg1 [lemma, in mathcomp.fingroup.gproduct]
+cprodJ [lemma, in mathcomp.fingroup.gproduct]
+cprodm [definition, in mathcomp.fingroup.gproduct]
+cprodmE [lemma, in mathcomp.fingroup.gproduct]
+cprodmEl [lemma, in mathcomp.fingroup.gproduct]
+cprodmEr [lemma, in mathcomp.fingroup.gproduct]
+cprodm_actf [lemma, in mathcomp.fingroup.gproduct]
+cprodm_sub [lemma, in mathcomp.fingroup.gproduct]
+cprodm_norm [lemma, in mathcomp.fingroup.gproduct]
+cprodP [lemma, in mathcomp.fingroup.gproduct]
+cprodW [lemma, in mathcomp.fingroup.gproduct]
+cprodWC [lemma, in mathcomp.fingroup.gproduct]
+cprodWpp [lemma, in mathcomp.fingroup.gproduct]
+cprodWY [lemma, in mathcomp.fingroup.gproduct]
+cprod_card_dprod [lemma, in mathcomp.fingroup.gproduct]
+cprod_modr [lemma, in mathcomp.fingroup.gproduct]
+cprod_modl [lemma, in mathcomp.fingroup.gproduct]
+cprod_ntriv [lemma, in mathcomp.fingroup.gproduct]
+cprod_normal2 [lemma, in mathcomp.fingroup.gproduct]
+cprod_abelem [lemma, in mathcomp.solvable.abelian]
+cprod_exponent [lemma, in mathcomp.solvable.abelian]
+cprod_extraspecial [lemma, in mathcomp.solvable.maximal]
+cprod_rowg [lemma, in mathcomp.character.mxabelem]
+cprod_nil [lemma, in mathcomp.solvable.nilpotent]
+cprod_by_uniq [lemma, in mathcomp.solvable.center]
+cprod_by [definition, in mathcomp.solvable.center]
+cprod_by_def [definition, in mathcomp.solvable.center]
+cprod_by_key [lemma, in mathcomp.solvable.center]
+cprod_center_id [lemma, in mathcomp.solvable.center]
+cprod0g [lemma, in mathcomp.fingroup.gproduct]
+cprod1g [lemma, in mathcomp.fingroup.gproduct]
+CratP [lemma, in mathcomp.field.algC]
+CratrE [definition, in mathcomp.field.algC]
+Crat_aut [lemma, in mathcomp.field.algC]
+Crat_divring_closed [lemma, in mathcomp.field.algC]
+Crat_key [lemma, in mathcomp.field.algC]
+Crat_rat [lemma, in mathcomp.field.algC]
+Crat_spanM [lemma, in mathcomp.field.algnum]
+Crat_spanZ [lemma, in mathcomp.field.algnum]
+Crat_span_zmod_closed [lemma, in mathcomp.field.algnum]
+Crat_span_key [lemma, in mathcomp.field.algnum]
+Crat_spanP [lemma, in mathcomp.field.algnum]
+Crat_span [definition, in mathcomp.field.algnum]
+Crat_span_subproof [lemma, in mathcomp.field.algnum]
+Crat0 [lemma, in mathcomp.field.algC]
+Crat1 [lemma, in mathcomp.field.algC]
+Creal_Crat [lemma, in mathcomp.field.algC]
+Creal_Cnat [lemma, in mathcomp.field.algC]
+Creal_Cint [lemma, in mathcomp.field.algC]
+Creal0 [lemma, in mathcomp.field.algC]
+Creal1 [lemma, in mathcomp.field.algC]
+critical [definition, in mathcomp.solvable.maximal]
+critical_p_stab_Aut [lemma, in mathcomp.solvable.maximal]
+critical_class2 [lemma, in mathcomp.solvable.maximal]
+critical_extraspecial [lemma, in mathcomp.solvable.maximal]
+CtoQ [abbreviation, in mathcomp.field.algC]
+cube [definition, in mathcomp.solvable.burnside_app]
+cube_coloring_number24 [definition, in mathcomp.solvable.burnside_app]
+curry_mxvec_bij [lemma, in mathcomp.algebra.matrix]
+curry_imset2r [lemma, in mathcomp.ssreflect.finset]
+curry_imset2l [lemma, in mathcomp.ssreflect.finset]
+curry_imset2X [lemma, in mathcomp.ssreflect.finset]
+cycle [definition, in mathcomp.ssreflect.path]
+cycle [definition, in mathcomp.fingroup.fingroup]
+CycleArc [section, in mathcomp.ssreflect.path]
+CycleArc.T [variable, in mathcomp.ssreflect.path]
+cycleJ [lemma, in mathcomp.fingroup.fingroup]
+cyclem [definition, in mathcomp.solvable.cyclic]
+cycleM [lemma, in mathcomp.solvable.cyclic]
+cyclemM [lemma, in mathcomp.solvable.cyclic]
+cycleMsub [lemma, in mathcomp.solvable.cyclic]
+cycleP [lemma, in mathcomp.fingroup.fingroup]
+cyclePmin [lemma, in mathcomp.fingroup.fingroup]
+Cycles [section, in mathcomp.fingroup.fingroup]
+CycleSubGroup [section, in mathcomp.solvable.cyclic]
+CycleSubGroup.gT [variable, in mathcomp.solvable.cyclic]
+Cycles.gT [variable, in mathcomp.fingroup.fingroup]
+cycleV [lemma, in mathcomp.fingroup.fingroup]
+cycleX [lemma, in mathcomp.fingroup.fingroup]
+cycle_constt [lemma, in mathcomp.solvable.pgroup]
+cycle_from_prev [lemma, in mathcomp.ssreflect.path]
+cycle_from_next [lemma, in mathcomp.ssreflect.path]
+cycle_prev [lemma, in mathcomp.ssreflect.path]
+cycle_next [lemma, in mathcomp.ssreflect.path]
+cycle_path [lemma, in mathcomp.ssreflect.path]
+cycle_repr_structure [lemma, in mathcomp.character.mxrepresentation]
+cycle_abelem [lemma, in mathcomp.solvable.abelian]
+cycle_abelian [lemma, in mathcomp.fingroup.fingroup]
+cycle_traject [lemma, in mathcomp.fingroup.fingroup]
+cycle_eq1 [lemma, in mathcomp.fingroup.fingroup]
+cycle_subG [lemma, in mathcomp.fingroup.fingroup]
+cycle_id [lemma, in mathcomp.fingroup.fingroup]
+cycle_orbit [lemma, in mathcomp.ssreflect.fingraph]
+cycle_orbit_in [lemma, in mathcomp.ssreflect.fingraph]
+cycle_subgroup_char [lemma, in mathcomp.solvable.cyclic]
+cycle_sub_group [lemma, in mathcomp.solvable.cyclic]
+cycle_generator [lemma, in mathcomp.solvable.cyclic]
+cycle_cyclic [lemma, in mathcomp.solvable.cyclic]
+cycle1 [lemma, in mathcomp.fingroup.fingroup]
+cycle2g [lemma, in mathcomp.fingroup.fingroup]
+cyclic [definition, in mathcomp.solvable.cyclic]
+Cyclic [section, in mathcomp.solvable.cyclic]
+cyclic [library]
+CyclicAutomorphism [section, in mathcomp.solvable.cyclic]
+CyclicAutomorphism.CycleAutomorphism [section, in mathcomp.solvable.cyclic]
+CyclicAutomorphism.CycleAutomorphism.a [variable, in mathcomp.solvable.cyclic]
+CyclicAutomorphism.CycleAutomorphism.CycleMorphism [section, in mathcomp.solvable.cyclic]
+CyclicAutomorphism.CycleAutomorphism.CycleMorphism.n [variable, in mathcomp.solvable.cyclic]
+CyclicAutomorphism.CycleAutomorphism.ZpUnitMorphism [section, in mathcomp.solvable.cyclic]
+CyclicAutomorphism.CycleAutomorphism.ZpUnitMorphism.u [variable, in mathcomp.solvable.cyclic]
+CyclicAutomorphism.G [variable, in mathcomp.solvable.cyclic]
+CyclicAutomorphism.gT [variable, in mathcomp.solvable.cyclic]
+cyclicJ [lemma, in mathcomp.solvable.cyclic]
+cyclicM [lemma, in mathcomp.solvable.cyclic]
+cyclicP [lemma, in mathcomp.solvable.cyclic]
+CyclicProps [section, in mathcomp.solvable.cyclic]
+CyclicProps.gT [variable, in mathcomp.solvable.cyclic]
+cyclicS [lemma, in mathcomp.solvable.cyclic]
+cyclicY [lemma, in mathcomp.solvable.cyclic]
+cyclic_mx_sub [lemma, in mathcomp.character.mxrepresentation]
+cyclic_mx_module [lemma, in mathcomp.character.mxrepresentation]
+cyclic_mx_eq0 [lemma, in mathcomp.character.mxrepresentation]
+cyclic_mx_id [lemma, in mathcomp.character.mxrepresentation]
+cyclic_mxP [lemma, in mathcomp.character.mxrepresentation]
+cyclic_mx [definition, in mathcomp.character.mxrepresentation]
+cyclic_SCN [lemma, in mathcomp.solvable.extremal]
+cyclic_pgroup_Aut_structure [lemma, in mathcomp.solvable.extremal]
+cyclic_pgroup_dprod_trivg [lemma, in mathcomp.solvable.abelian]
+cyclic_abelem_prime [lemma, in mathcomp.solvable.abelian]
+cyclic_nilpotent_quo_der1_cyclic [lemma, in mathcomp.solvable.nilpotent]
+cyclic_factor_abelian [lemma, in mathcomp.solvable.center]
+cyclic_center_factor_abelian [lemma, in mathcomp.solvable.center]
+cyclic_metacyclic [lemma, in mathcomp.solvable.cyclic]
+cyclic_small [lemma, in mathcomp.solvable.cyclic]
+cyclic_dprod [lemma, in mathcomp.solvable.cyclic]
+cyclic_abelian [lemma, in mathcomp.solvable.cyclic]
+Cyclic.gT [variable, in mathcomp.solvable.cyclic]
+Cyclic.Zpm [section, in mathcomp.solvable.cyclic]
+Cyclic.Zpm.a [variable, in mathcomp.solvable.cyclic]
+cyclic1 [lemma, in mathcomp.solvable.cyclic]
+Cyclotomic [definition, in mathcomp.field.cyclotomic]
+cyclotomic [definition, in mathcomp.field.cyclotomic]
+cyclotomic [library]
+CyclotomicPoly [section, in mathcomp.field.cyclotomic]
+CyclotomicPoly.Field [section, in mathcomp.field.cyclotomic]
+CyclotomicPoly.Field.F [variable, in mathcomp.field.cyclotomic]
+CyclotomicPoly.Field.n [variable, in mathcomp.field.cyclotomic]
+CyclotomicPoly.Field.n_gt0 [variable, in mathcomp.field.cyclotomic]
+CyclotomicPoly.Field.prim_z [variable, in mathcomp.field.cyclotomic]
+CyclotomicPoly.Field.z [variable, in mathcomp.field.cyclotomic]
+CyclotomicPoly.Ring [section, in mathcomp.field.cyclotomic]
+CyclotomicPoly.Ring.R [variable, in mathcomp.field.cyclotomic]
+Cyclotomic_monic [lemma, in mathcomp.field.cyclotomic]
+cyclotomic_monic [lemma, in mathcomp.field.cyclotomic]
+Cyclotomic0 [lemma, in mathcomp.field.cyclotomic]
+C_prim_root_exists [lemma, in mathcomp.field.cyclotomic]
+c0 [definition, in mathcomp.solvable.burnside_app]
+c1 [definition, in mathcomp.solvable.burnside_app]
+c2 [definition, in mathcomp.solvable.burnside_app]
+c3 [definition, in mathcomp.solvable.burnside_app]
+
| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +