| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 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 [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_pfamily [lemma, in mathcomp.ssreflect.finfun]
-card_dep_ffun [lemma, in mathcomp.ssreflect.finfun]
-card_family [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]
-cfIirr_key [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]
-choiceMixin [lemma, in mathcomp.ssreflect.finfun]
-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 [module, in mathcomp.field.closed_field]
-ClosedFieldQE.abstrX [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.abstrXP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.abstrX_bigmul [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.abstrX_mulM [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.abstrX1 [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.amulXnT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.bigmap_id [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.bind [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.ClosedFieldQE [section, in mathcomp.field.closed_field]
-ClosedFieldQE.ClosedFieldQE.F [variable, in mathcomp.field.closed_field]
-ClosedFieldQE.ClosedFieldQE.F_closed [variable, in mathcomp.field.closed_field]
-_ ->_ _ _ [notation, in mathcomp.field.closed_field]
-'if _ then _ else _ [notation, in mathcomp.field.closed_field]
-'let _ <- _ ; _ [notation, in mathcomp.field.closed_field]
-ClosedFieldQE.cps [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.cpsif [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.eval [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_bigmul [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_poly1 [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_poly_mulM [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_natmulpT [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_opppT [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_mulpT [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_sumpT [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_amulXnT [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_lift [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.eval_poly [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.ex_elim_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.ex_elim [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.ex_elim_seq_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.ex_elim_seqP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.ex_elim_seq [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.fF [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.holds_ex_elim [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.holds_conjn [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.holds_conj [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.isnull [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.isnullP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.isnull_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.lead_coefT_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.lead_coefTP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.lead_coefT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.lift [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.lt_sizeT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.Mixin [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.mulpT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.natmulpT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.opppT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.polyF [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.qf [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.qf_cps_if [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.qf_cps_bind [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.qf_cps_ret [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.qf_cps [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.qf_red_cps [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.qf_eval [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.qf_simpl [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rabstrX [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.ramulXnT [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rdivpT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rdvdpT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.redivpT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.redivpTP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.redivpT_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.redivp_rec_loopP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.redivp_rec_loopT_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.redivp_rec_loopTP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.redivp_rec_loop [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.redivp_rec_loopT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.ret [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdpT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdpTP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdpTs [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdpTsP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdpTs_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdpT_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdp_loopT_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdp_loopP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdp_loopT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rgcdp_loop [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rgdcopT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rgdcopTP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgdcopT_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgdcop_recT_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgdcop_recTP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rgdcop_recT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rmodpT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rmulpT [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rpoly [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rpoly_map_mul [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rscalpT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.rseq_poly_map [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rsumpT [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.rterm [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.sizeT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.sizeTP [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.sizeT_qf [lemma, in mathcomp.field.closed_field]
-ClosedFieldQE.sumpT [definition, in mathcomp.field.closed_field]
-ClosedFieldQE.tF [abbreviation, in mathcomp.field.closed_field]
-ClosedFieldQE.wf_ex_elim [lemma, 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_field_QEMixin [abbreviation, 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]
-codom_tffun [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_comp_poly [lemma, in mathcomp.algebra.poly]
-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]
-companionmx [definition, in mathcomp.algebra.mxpoly]
-companionmxK [lemma, in mathcomp.algebra.mxpoly]
-companion_map_poly [lemma, in mathcomp.algebra.mxpoly]
-comparable [definition, in mathcomp.ssreflect.eqtype]
-comparableMixin [definition, in mathcomp.ssreflect.eqtype]
-ComparableType [section, in mathcomp.ssreflect.eqtype]
-ComparableType.compare_T [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_poly_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_perms [abbreviation, in mathcomp.ssreflect.seq]
-cons_perms_ [definition, in mathcomp.ssreflect.seq]
-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_eq_neq [lemma, in mathcomp.ssreflect.eqtype]
-contra_neq_eq [lemma, in mathcomp.ssreflect.eqtype]
-contra_neq [lemma, in mathcomp.ssreflect.eqtype]
-contra_eq [lemma, in mathcomp.ssreflect.eqtype]
-contra_neqT [lemma, in mathcomp.ssreflect.eqtype]
-contra_neqF [lemma, in mathcomp.ssreflect.eqtype]
-contra_neqN [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.closed_field]
-countable_field_extension [lemma, in mathcomp.field.closed_field]
-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]
-countMixin [lemma, in mathcomp.ssreflect.finfun]
-CountRing [module, in mathcomp.algebra.countalg]
-CountRing.ClosedField [module, in mathcomp.algebra.countalg]
-CountRing.ClosedField.base [projection, in mathcomp.algebra.countalg]
-CountRing.ClosedField.base2 [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.choiceType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.class [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.Class [constructor, in mathcomp.algebra.countalg]
-CountRing.ClosedField.ClassDef [section, in mathcomp.algebra.countalg]
-CountRing.ClosedField.ClassDef.cT [variable, in mathcomp.algebra.countalg]
-CountRing.ClosedField.ClassDef.xT [variable, in mathcomp.algebra.countalg]
-CountRing.ClosedField.class_of [record, in mathcomp.algebra.countalg]
-CountRing.ClosedField.closedFieldType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.comRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.comUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.countComUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.countDecFieldType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.countFieldType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.countIdomainType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.countType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.decFieldType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.eqType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.Exports [module, in mathcomp.algebra.countalg]
-CountRing.ClosedField.Exports.countClosedFieldType [abbreviation, in mathcomp.algebra.countalg]
-[ countClosedFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
-CountRing.ClosedField.fieldType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.idomainType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.join_countDecFieldType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.join_countFieldType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.join_countIdomainType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.join_countComUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.join_countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.join_countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.join_countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.join_countType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.mixin [projection, in mathcomp.algebra.countalg]
-CountRing.ClosedField.pack [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.Pack [constructor, in mathcomp.algebra.countalg]
-CountRing.ClosedField.ringType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.sort [projection, in mathcomp.algebra.countalg]
-CountRing.ClosedField.type [record, in mathcomp.algebra.countalg]
-CountRing.ClosedField.unitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ClosedField.xclass [abbreviation, in mathcomp.algebra.countalg]
-CountRing.ClosedField.zmodType [definition, in mathcomp.algebra.countalg]
-CountRing.cnt_ [abbreviation, in mathcomp.algebra.countalg]
-CountRing.ComRing [module, in mathcomp.algebra.countalg]
-CountRing.ComRing.base [projection, in mathcomp.algebra.countalg]
-CountRing.ComRing.base2 [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.choiceType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.class [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.Class [constructor, in mathcomp.algebra.countalg]
-CountRing.ComRing.ClassDef [section, in mathcomp.algebra.countalg]
-CountRing.ComRing.ClassDef.cT [variable, in mathcomp.algebra.countalg]
-CountRing.ComRing.ClassDef.xT [variable, in mathcomp.algebra.countalg]
-CountRing.ComRing.class_of [record, in mathcomp.algebra.countalg]
-CountRing.ComRing.comRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.countType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.eqType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.Exports [module, in mathcomp.algebra.countalg]
-CountRing.ComRing.Exports.countComRingType [abbreviation, in mathcomp.algebra.countalg]
-[ countComRingType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
-CountRing.ComRing.join_countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.join_countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.join_countType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.mixin [projection, in mathcomp.algebra.countalg]
-CountRing.ComRing.pack [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.Pack [constructor, in mathcomp.algebra.countalg]
-CountRing.ComRing.ringType [definition, in mathcomp.algebra.countalg]
-CountRing.ComRing.sort [projection, in mathcomp.algebra.countalg]
-CountRing.ComRing.type [record, in mathcomp.algebra.countalg]
-CountRing.ComRing.xclass [abbreviation, in mathcomp.algebra.countalg]
-CountRing.ComRing.zmodType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing [module, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.base [projection, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.base2 [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.base3 [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.ccjoin_countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.choiceType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.cjoin_countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.class [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.Class [constructor, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.ClassDef [section, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.ClassDef.cT [variable, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.ClassDef.xT [variable, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.class_of [record, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.comRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.comUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.countType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.eqType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.Exports [module, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.Exports.countComUnitRingType [abbreviation, in mathcomp.algebra.countalg]
-[ countComUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.join_countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.join_countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.join_countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.join_countType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.mixin [projection, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.pack [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.Pack [constructor, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.ringType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.sort [projection, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.type [record, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.ujoin_countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.unitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.xclass [abbreviation, in mathcomp.algebra.countalg]
-CountRing.ComUnitRing.zmodType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField [module, in mathcomp.algebra.countalg]
-CountRing.DecidableField.base [projection, in mathcomp.algebra.countalg]
-CountRing.DecidableField.base2 [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.choiceType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.class [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.Class [constructor, in mathcomp.algebra.countalg]
-CountRing.DecidableField.ClassDef [section, in mathcomp.algebra.countalg]
-CountRing.DecidableField.ClassDef.cT [variable, in mathcomp.algebra.countalg]
-CountRing.DecidableField.ClassDef.xT [variable, in mathcomp.algebra.countalg]
-CountRing.DecidableField.class_of [record, in mathcomp.algebra.countalg]
-CountRing.DecidableField.comRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.comUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.countComUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.countFieldType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.countIdomainType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.countType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.decFieldType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.eqType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.Exports [module, in mathcomp.algebra.countalg]
-CountRing.DecidableField.Exports.countDecFieldType [abbreviation, in mathcomp.algebra.countalg]
-[ countDecFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
-CountRing.DecidableField.fieldType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.idomainType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.join_countFieldType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.join_countIdomainType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.join_countComUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.join_countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.join_countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.join_countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.join_countType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.mixin [projection, in mathcomp.algebra.countalg]
-CountRing.DecidableField.pack [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.Pack [constructor, in mathcomp.algebra.countalg]
-CountRing.DecidableField.ringType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.sort [projection, in mathcomp.algebra.countalg]
-CountRing.DecidableField.type [record, in mathcomp.algebra.countalg]
-CountRing.DecidableField.unitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.DecidableField.xclass [abbreviation, in mathcomp.algebra.countalg]
-CountRing.DecidableField.zmodType [definition, in mathcomp.algebra.countalg]
-CountRing.do_pack [abbreviation, in mathcomp.algebra.countalg]
-CountRing.Field [module, in mathcomp.algebra.countalg]
-CountRing.Field.base [projection, in mathcomp.algebra.countalg]
-CountRing.Field.base2 [definition, in mathcomp.algebra.countalg]
-CountRing.Field.choiceType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.class [definition, in mathcomp.algebra.countalg]
-CountRing.Field.Class [constructor, in mathcomp.algebra.countalg]
-CountRing.Field.ClassDef [section, in mathcomp.algebra.countalg]
-CountRing.Field.ClassDef.cT [variable, in mathcomp.algebra.countalg]
-CountRing.Field.ClassDef.xT [variable, in mathcomp.algebra.countalg]
-CountRing.Field.class_of [record, in mathcomp.algebra.countalg]
-CountRing.Field.comRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.comUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.countComUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.countIdomainType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.countType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.eqType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.Exports [module, in mathcomp.algebra.countalg]
-CountRing.Field.Exports.countFieldType [abbreviation, in mathcomp.algebra.countalg]
-[ countFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
-CountRing.Field.fieldType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.idomainType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.join_countIdomainType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.join_countComUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.join_countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.join_countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.join_countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.join_countType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.mixin [projection, in mathcomp.algebra.countalg]
-CountRing.Field.pack [definition, in mathcomp.algebra.countalg]
-CountRing.Field.Pack [constructor, in mathcomp.algebra.countalg]
-CountRing.Field.ringType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.sort [projection, in mathcomp.algebra.countalg]
-CountRing.Field.type [record, in mathcomp.algebra.countalg]
-CountRing.Field.unitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.Field.xclass [abbreviation, in mathcomp.algebra.countalg]
-CountRing.Field.zmodType [definition, in mathcomp.algebra.countalg]
-CountRing.Generic [section, in mathcomp.algebra.countalg]
-CountRing.Generic.base_class [variable, in mathcomp.algebra.countalg]
-CountRing.Generic.base_sort [variable, in mathcomp.algebra.countalg]
-CountRing.Generic.base_of [variable, in mathcomp.algebra.countalg]
-CountRing.Generic.base_type [variable, in mathcomp.algebra.countalg]
-CountRing.Generic.Class [variable, in mathcomp.algebra.countalg]
-CountRing.Generic.class_of [variable, in mathcomp.algebra.countalg]
-CountRing.Generic.Pack [variable, in mathcomp.algebra.countalg]
-CountRing.Generic.type [variable, in mathcomp.algebra.countalg]
-CountRing.gen_pack [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain [module, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.base [projection, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.base2 [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.choiceType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.class [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.Class [constructor, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.ClassDef [section, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.ClassDef.cT [variable, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.ClassDef.xT [variable, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.class_of [record, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.comRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.comUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.countComUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.countType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.eqType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.Exports [module, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.Exports.countIdomainType [abbreviation, in mathcomp.algebra.countalg]
-[ countIdomainType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.idomainType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.join_countComUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.join_countComRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.join_countUnitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.join_countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.join_countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.join_countType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.mixin [projection, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.pack [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.Pack [constructor, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.ringType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.sort [projection, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.type [record, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.unitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.xclass [abbreviation, in mathcomp.algebra.countalg]
-CountRing.IntegralDomain.zmodType [definition, in mathcomp.algebra.countalg]
-CountRing.mixin_of [abbreviation, in mathcomp.algebra.countalg]
-CountRing.Ring [module, in mathcomp.algebra.countalg]
-CountRing.Ring.base [projection, in mathcomp.algebra.countalg]
-CountRing.Ring.base2 [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.choiceType [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.class [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.Class [constructor, in mathcomp.algebra.countalg]
-CountRing.Ring.ClassDef [section, in mathcomp.algebra.countalg]
-CountRing.Ring.ClassDef.cT [variable, in mathcomp.algebra.countalg]
-CountRing.Ring.ClassDef.xT [variable, in mathcomp.algebra.countalg]
-CountRing.Ring.class_of [record, in mathcomp.algebra.countalg]
-CountRing.Ring.countType [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.eqType [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.Exports [module, in mathcomp.algebra.countalg]
-CountRing.Ring.Exports.countRingType [abbreviation, in mathcomp.algebra.countalg]
-[ countRingType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
-CountRing.Ring.join_countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.join_countType [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.mixin [projection, in mathcomp.algebra.countalg]
-CountRing.Ring.pack [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.Pack [constructor, in mathcomp.algebra.countalg]
-CountRing.Ring.ringType [definition, in mathcomp.algebra.countalg]
-CountRing.Ring.sort [projection, in mathcomp.algebra.countalg]
-CountRing.Ring.type [record, in mathcomp.algebra.countalg]
-CountRing.Ring.xclass [abbreviation, in mathcomp.algebra.countalg]
-CountRing.Ring.zmodType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing [module, in mathcomp.algebra.countalg]
-CountRing.UnitRing.base [projection, in mathcomp.algebra.countalg]
-CountRing.UnitRing.base2 [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.choiceType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.class [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.Class [constructor, in mathcomp.algebra.countalg]
-CountRing.UnitRing.ClassDef [section, in mathcomp.algebra.countalg]
-CountRing.UnitRing.ClassDef.cT [variable, in mathcomp.algebra.countalg]
-CountRing.UnitRing.ClassDef.xT [variable, in mathcomp.algebra.countalg]
-CountRing.UnitRing.class_of [record, in mathcomp.algebra.countalg]
-CountRing.UnitRing.countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.countType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.eqType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.Exports [module, in mathcomp.algebra.countalg]
-CountRing.UnitRing.Exports.countUnitRingType [abbreviation, in mathcomp.algebra.countalg]
-[ countUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
-CountRing.UnitRing.join_countRingType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.join_countZmodType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.join_countType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.mixin [projection, in mathcomp.algebra.countalg]
-CountRing.UnitRing.pack [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.Pack [constructor, in mathcomp.algebra.countalg]
-CountRing.UnitRing.ringType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.sort [projection, in mathcomp.algebra.countalg]
-CountRing.UnitRing.type [record, in mathcomp.algebra.countalg]
-CountRing.UnitRing.unitRingType [definition, in mathcomp.algebra.countalg]
-CountRing.UnitRing.xclass [abbreviation, in mathcomp.algebra.countalg]
-CountRing.UnitRing.zmodType [definition, in mathcomp.algebra.countalg]
-CountRing.Zmodule [module, in mathcomp.algebra.countalg]
-CountRing.Zmodule.base [projection, in mathcomp.algebra.countalg]
-CountRing.Zmodule.choiceType [definition, in mathcomp.algebra.countalg]
-CountRing.Zmodule.class [definition, in mathcomp.algebra.countalg]
-CountRing.Zmodule.Class [constructor, in mathcomp.algebra.countalg]
-CountRing.Zmodule.ClassDef [section, in mathcomp.algebra.countalg]
-CountRing.Zmodule.ClassDef.cT [variable, in mathcomp.algebra.countalg]
-CountRing.Zmodule.ClassDef.xT [variable, in mathcomp.algebra.countalg]
-CountRing.Zmodule.class_of [record, in mathcomp.algebra.countalg]
-CountRing.Zmodule.countType [definition, in mathcomp.algebra.countalg]
-CountRing.Zmodule.eqType [definition, in mathcomp.algebra.countalg]
-CountRing.Zmodule.Exports [module, in mathcomp.algebra.countalg]
-CountRing.Zmodule.Exports.countZmodType [abbreviation, in mathcomp.algebra.countalg]
-[ countZmodType of _ ] (form_scope) [notation, in mathcomp.algebra.countalg]
-CountRing.Zmodule.join_countType [definition, in mathcomp.algebra.countalg]
-CountRing.Zmodule.mixin [projection, in mathcomp.algebra.countalg]
-CountRing.Zmodule.pack [definition, in mathcomp.algebra.countalg]
-CountRing.Zmodule.Pack [constructor, in mathcomp.algebra.countalg]
-CountRing.Zmodule.sort [projection, in mathcomp.algebra.countalg]
-CountRing.Zmodule.type [record, in mathcomp.algebra.countalg]
-CountRing.Zmodule.xclass [abbreviation, in mathcomp.algebra.countalg]
-CountRing.Zmodule.zmodType [definition, in mathcomp.algebra.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_mem [abbreviation, in mathcomp.ssreflect.seq]
-count_rev [lemma, 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_nseq [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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -