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

(24263 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

(1399 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

(226 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

(3670 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(89 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12297 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

(383 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

(114 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

(279 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

(1169 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

(742 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

(3657 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

(193 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_void [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_le1P [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]
card1P [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]
cofixset [definition, in mathcomp.ssreflect.finset]
cofixsetK [lemma, in mathcomp.ssreflect.finset]
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_cycle [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_catC [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_cycle [lemma, in mathcomp.ssreflect.fingraph]
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

(24263 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

(1399 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

(226 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

(3670 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(89 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12297 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

(383 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

(114 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

(279 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

(1169 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

(742 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

(3657 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

(193 entries)