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

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

(1892 entries)

Binder 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

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

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

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

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

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

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

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

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

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

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

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

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

(36 entries)

---

Q

qact [definition, in mathcomp.fingroup.action]
qactE [lemma, in mathcomp.fingroup.action]
qactEcond [lemma, in mathcomp.fingroup.action]
qactJ [lemma, in mathcomp.fingroup.action]
qacts_coset [lemma, in mathcomp.solvable.jordanholder]
qacts_cosetpre [lemma, in mathcomp.solvable.jordanholder]
qact_dom_doms [lemma, in mathcomp.solvable.jordanholder]
qact_domE [lemma, in mathcomp.fingroup.action]
qact_is_groupAction [lemma, in mathcomp.fingroup.action]
qact_proof [lemma, in mathcomp.fingroup.action]
qact_subdomE [lemma, in mathcomp.fingroup.action]
qact_dom_group [definition, in mathcomp.fingroup.action]
qact_dom [definition, in mathcomp.fingroup.action]
qev:1671 [binder, in mathcomp.algebra.ssralg]
qev:1701 [binder, in mathcomp.algebra.ssralg]
qfpoly [definition, in mathcomp.field.qfpoly]
qfpoly [library]
qfpoly_splitting_field_type [definition, in mathcomp.field.qfpoly]
qfpoly_const [definition, in mathcomp.field.qfpoly]
qf_eval [abbreviation, in mathcomp.character.mxrepresentation]
qf_form [abbreviation, in mathcomp.character.mxrepresentation]
qf:1971 [binder, in mathcomp.algebra.ssralg]
qf:1974 [binder, in mathcomp.algebra.ssralg]
qidmx [definition, in mathcomp.algebra.mxalgebra]
Qint [abbreviation, in mathcomp.algebra.rat]
QintP [abbreviation, in mathcomp.algebra.rat]
Qint_dvdz [lemma, in mathcomp.algebra.intdiv]
Qint_def [lemma, in mathcomp.algebra.rat]
qisom [definition, in mathcomp.fingroup.quotient]
qisomE [lemma, in mathcomp.fingroup.quotient]
qisom_inj [lemma, in mathcomp.fingroup.quotient]
qisom_isog [lemma, in mathcomp.fingroup.quotient]
qisom_isom [lemma, in mathcomp.fingroup.quotient]
qisom_morphism [definition, in mathcomp.fingroup.quotient]
qisom_restr_proof [lemma, in mathcomp.fingroup.quotient]
qisom_ker_proof [lemma, in mathcomp.fingroup.quotient]
qlogp [definition, in mathcomp.field.qfpoly]
qlogpD [lemma, in mathcomp.field.qfpoly]
qlogp_eq0 [lemma, in mathcomp.field.qfpoly]
qlogp_qX [lemma, in mathcomp.field.qfpoly]
qlogp_lt [lemma, in mathcomp.field.qfpoly]
qlogp0 [lemma, in mathcomp.field.qfpoly]
qlogp1 [lemma, in mathcomp.field.qfpoly]
Qmorphism [abbreviation, in mathcomp.field.algebraics_fundamentals]
Qnat [abbreviation, in mathcomp.algebra.rat]
QnatP [abbreviation, in mathcomp.algebra.rat]
Qnat_dvd [lemma, in mathcomp.algebra.intdiv]
Qnat_def [abbreviation, in mathcomp.algebra.rat]
QnC:10 [binder, in mathcomp.character.integral_char]
QnC:107 [binder, in mathcomp.field.algnum]
QnC:5 [binder, in mathcomp.character.integral_char]
Qn_aut_exists [lemma, in mathcomp.field.algnum]
Qn:106 [binder, in mathcomp.field.algnum]
Qn:3 [binder, in mathcomp.character.integral_char]
Qn:4 [binder, in mathcomp.character.integral_char]
qpoly [definition, in mathcomp.algebra.qpoly]
Qpoly [section, in mathcomp.algebra.qpoly]
qpoly [library]
qpolyC [definition, in mathcomp.algebra.qpoly]
qpolyCD [lemma, in mathcomp.algebra.qpoly]
qpolyCE [lemma, in mathcomp.algebra.qpoly]
qpolyCM [lemma, in mathcomp.algebra.qpoly]
qpolyCN [lemma, in mathcomp.algebra.qpoly]
qpolyC_is_multiplicative [lemma, in mathcomp.algebra.qpoly]
qpolyC_is_additive [lemma, in mathcomp.algebra.qpoly]
qpolyC_natr [lemma, in mathcomp.algebra.qpoly]
qpolyC_proof [lemma, in mathcomp.algebra.qpoly]
qpolyC0 [lemma, in mathcomp.algebra.qpoly]
QpolyProp [section, in mathcomp.algebra.qpoly]
QpolyProp.h [variable, in mathcomp.algebra.qpoly]
QpolyProp.R [variable, in mathcomp.algebra.qpoly]
'qX [notation, in mathcomp.algebra.qpoly]
qpolyX [definition, in mathcomp.algebra.qpoly]
qpolyXE [lemma, in mathcomp.algebra.qpoly]
qpoly_inv0 [lemma, in mathcomp.field.qfpoly]
qpoly_mulVp [lemma, in mathcomp.field.qfpoly]
qpoly_inv_out [lemma, in mathcomp.algebra.qpoly]
qpoly_intro_unit [lemma, in mathcomp.algebra.qpoly]
qpoly_mulzV [lemma, in mathcomp.algebra.qpoly]
qpoly_mulVz [lemma, in mathcomp.algebra.qpoly]
qpoly_inv [definition, in mathcomp.algebra.qpoly]
qpoly_scaleAr [lemma, in mathcomp.algebra.qpoly]
qpoly_scaleAl [lemma, in mathcomp.algebra.qpoly]
qpoly_scaleDl [lemma, in mathcomp.algebra.qpoly]
qpoly_scaleDr [lemma, in mathcomp.algebra.qpoly]
qpoly_scale1l [lemma, in mathcomp.algebra.qpoly]
qpoly_scaleA [lemma, in mathcomp.algebra.qpoly]
qpoly_scale [definition, in mathcomp.algebra.qpoly]
qpoly_mul_addl [lemma, in mathcomp.algebra.qpoly]
qpoly_mul_addr [lemma, in mathcomp.algebra.qpoly]
qpoly_mulA [lemma, in mathcomp.algebra.qpoly]
qpoly_mulC [lemma, in mathcomp.algebra.qpoly]
qpoly_nontrivial [lemma, in mathcomp.algebra.qpoly]
qpoly_mulz1 [lemma, in mathcomp.algebra.qpoly]
qpoly_mul1z [lemma, in mathcomp.algebra.qpoly]
qpoly_mul [definition, in mathcomp.algebra.qpoly]
Qpoly.h [variable, in mathcomp.algebra.qpoly]
Qpoly.R [variable, in mathcomp.algebra.qpoly]
qpoly1 [definition, in mathcomp.algebra.qpoly]
qq1:11 [binder, in mathcomp.algebra.polydiv]
qq1:132 [binder, in mathcomp.field.closed_field]
qq1:144 [binder, in mathcomp.field.closed_field]
qq:1045 [binder, in mathcomp.algebra.polydiv]
qq:125 [binder, in mathcomp.field.closed_field]
qq:139 [binder, in mathcomp.field.closed_field]
qq:149 [binder, in mathcomp.field.closed_field]
qq:156 [binder, in mathcomp.field.closed_field]
qq:165 [binder, in mathcomp.field.closed_field]
qq:172 [binder, in mathcomp.algebra.polydiv]
qq:177 [binder, in mathcomp.field.closed_field]
qq:182 [binder, in mathcomp.field.closed_field]
qq:206 [binder, in mathcomp.field.closed_field]
qq:212 [binder, in mathcomp.field.closed_field]
qq:493 [binder, in mathcomp.algebra.polydiv]
qq:502 [binder, in mathcomp.algebra.polydiv]
qq:6 [binder, in mathcomp.algebra.polydiv]
qq:66 [binder, in mathcomp.algebra.polydiv]
qq:75 [binder, in mathcomp.algebra.polydiv]
qq:808 [binder, in mathcomp.algebra.polydiv]
QrC:201 [binder, in mathcomp.field.algnum]
QrC:205 [binder, in mathcomp.field.algnum]
QRing [section, in mathcomp.algebra.qpoly]
QRing.A [variable, in mathcomp.algebra.qpoly]
QRing.h [variable, in mathcomp.algebra.qpoly]
Qr:193 [binder, in mathcomp.field.algnum]
Qr:194 [binder, in mathcomp.field.algnum]
QsC:188 [binder, in mathcomp.field.algnum]
QsC:26 [binder, in mathcomp.field.algnum]
QsC:30 [binder, in mathcomp.field.algnum]
Qs:187 [binder, in mathcomp.field.algnum]
Qs:25 [binder, in mathcomp.field.algnum]
Qs:2765 [binder, in mathcomp.ssreflect.seq]
Qs:29 [binder, in mathcomp.field.algnum]
qs:370 [binder, in mathcomp.ssreflect.div]
qs:376 [binder, in mathcomp.ssreflect.div]
qT [abbreviation, in mathcomp.field.qfpoly]
QtoC [abbreviation, in mathcomp.field.cyclotomic]
QtoC [abbreviation, in mathcomp.field.algC]
QtoC [abbreviation, in mathcomp.field.algnum]
QtoCm:122 [binder, in mathcomp.field.algC]
QtoC:16 [binder, in mathcomp.field.algebraics_fundamentals]
QtoC:2 [binder, in mathcomp.field.algebraics_fundamentals]
qT:118 [binder, in mathcomp.ssreflect.generic_quotient]
qT:120 [binder, in mathcomp.ssreflect.generic_quotient]
qT:135 [binder, in mathcomp.ssreflect.generic_quotient]
qT:137 [binder, in mathcomp.ssreflect.generic_quotient]
qT:139 [binder, in mathcomp.ssreflect.generic_quotient]
qT:2 [binder, in mathcomp.ssreflect.generic_quotient]
qT:34 [binder, in mathcomp.ssreflect.generic_quotient]
qT:9 [binder, in mathcomp.ssreflect.generic_quotient]
QuantifierCombinators [section, in mathcomp.ssreflect.fintype]
QuantifierCombinators.P [variable, in mathcomp.ssreflect.fintype]
QuantifierCombinators.PP [variable, in mathcomp.ssreflect.fintype]
QuantifierCombinators.T [variable, in mathcomp.ssreflect.fintype]
QuantifierCombinators.viewP [variable, in mathcomp.ssreflect.fintype]
Quantifiers [section, in mathcomp.ssreflect.fintype]
Quantifiers.rT [variable, in mathcomp.ssreflect.fintype]
Quantifiers.T [variable, in mathcomp.ssreflect.fintype]
Quaternion [constructor, in mathcomp.solvable.extremal]
quaternion_classP [lemma, in mathcomp.solvable.extremal]
quaternion_structure [lemma, in mathcomp.solvable.extremal]
quaternion_unlock [definition, in mathcomp.solvable.extremal]
quaternion_kernel [definition, in mathcomp.solvable.extremal]
QuoMax [section, in mathcomp.solvable.gseries]
QuoMax.G [variable, in mathcomp.solvable.gseries]
QuoMax.gT [variable, in mathcomp.solvable.gseries]
QuoMax.H [variable, in mathcomp.solvable.gseries]
QuoMax.K [variable, in mathcomp.solvable.gseries]
quotient [definition, in mathcomp.fingroup.quotient]
Quotient [module, in mathcomp.algebra.ring_quotient]
quotient [library]
QuotientAbelem [section, in mathcomp.solvable.abelian]
QuotientAbelem.gT [variable, in mathcomp.solvable.abelian]
QuotientAbelem.p [variable, in mathcomp.solvable.abelian]
QuotientAction [section, in mathcomp.fingroup.action]
QuotientAction.aT [variable, in mathcomp.fingroup.action]
QuotientAction.D [variable, in mathcomp.fingroup.action]
QuotientAction.H [variable, in mathcomp.fingroup.action]
QuotientAction.rT [variable, in mathcomp.fingroup.action]
QuotientAction.to [variable, in mathcomp.fingroup.action]
quotientD [lemma, in mathcomp.fingroup.quotient]
QuotientDef [section, in mathcomp.ssreflect.generic_quotient]
QuotientDef.qT [variable, in mathcomp.ssreflect.generic_quotient]
QuotientDef.T [variable, in mathcomp.ssreflect.generic_quotient]
\pi [notation, in mathcomp.ssreflect.generic_quotient]
quotientDG [lemma, in mathcomp.fingroup.quotient]
quotientD1 [lemma, in mathcomp.fingroup.quotient]
quotientE [lemma, in mathcomp.fingroup.quotient]
quotientGI [lemma, in mathcomp.fingroup.quotient]
quotientGK [lemma, in mathcomp.fingroup.quotient]
quotientI [lemma, in mathcomp.fingroup.quotient]
quotientIG [lemma, in mathcomp.fingroup.quotient]
quotientInorm [lemma, in mathcomp.fingroup.quotient]
QuotientInternalProd [section, in mathcomp.fingroup.gproduct]
QuotientInternalProd.G [variable, in mathcomp.fingroup.gproduct]
QuotientInternalProd.gT [variable, in mathcomp.fingroup.gproduct]
QuotientInternalProd.H [variable, in mathcomp.fingroup.gproduct]
QuotientInternalProd.K [variable, in mathcomp.fingroup.gproduct]
QuotientInternalProd.M [variable, in mathcomp.fingroup.gproduct]
QuotientInternalProd.nMG [variable, in mathcomp.fingroup.gproduct]
quotientJ [lemma, in mathcomp.fingroup.quotient]
quotientK [lemma, in mathcomp.fingroup.quotient]
quotientMidl [lemma, in mathcomp.fingroup.quotient]
quotientMidr [lemma, in mathcomp.fingroup.quotient]
quotientMl [lemma, in mathcomp.fingroup.quotient]
QuotientMorphism [section, in mathcomp.fingroup.quotient]
QuotientMorphism.f [variable, in mathcomp.fingroup.quotient]
QuotientMorphism.G [variable, in mathcomp.fingroup.quotient]
QuotientMorphism.gT [variable, in mathcomp.fingroup.quotient]
QuotientMorphism.H [variable, in mathcomp.fingroup.quotient]
QuotientMorphism.nfHfG [variable, in mathcomp.fingroup.quotient]
QuotientMorphism.nHG [variable, in mathcomp.fingroup.quotient]
QuotientMorphism.nsHG [variable, in mathcomp.fingroup.quotient]
QuotientMorphism.rT [variable, in mathcomp.fingroup.quotient]
QuotientMorphism.sHG [variable, in mathcomp.fingroup.quotient]
quotientMr [lemma, in mathcomp.fingroup.quotient]
QuotientNil [section, in mathcomp.solvable.nilpotent]
QuotientNil.gT [variable, in mathcomp.solvable.nilpotent]
quotientR [lemma, in mathcomp.fingroup.quotient]
QuotientRank [section, in mathcomp.solvable.abelian]
QuotientRank.cGG [variable, in mathcomp.solvable.abelian]
QuotientRank.G [variable, in mathcomp.solvable.abelian]
QuotientRank.gT [variable, in mathcomp.solvable.abelian]
QuotientRank.H [variable, in mathcomp.solvable.abelian]
QuotientRank.p [variable, in mathcomp.solvable.abelian]
quotientS [lemma, in mathcomp.fingroup.quotient]
quotientSGK [lemma, in mathcomp.fingroup.quotient]
quotientSK [lemma, in mathcomp.fingroup.quotient]
QuotientSol [section, in mathcomp.solvable.nilpotent]
QuotientSol.gT [variable, in mathcomp.solvable.nilpotent]
QuotientSol.rT [variable, in mathcomp.solvable.nilpotent]
quotientS1 [lemma, in mathcomp.fingroup.quotient]
quotientT [lemma, in mathcomp.fingroup.quotient]
quotientU [lemma, in mathcomp.fingroup.quotient]
quotientV [lemma, in mathcomp.fingroup.quotient]
quotientY [lemma, in mathcomp.fingroup.quotient]
quotientYidl [lemma, in mathcomp.fingroup.quotient]
quotientYidr [lemma, in mathcomp.fingroup.quotient]
quotientYK [lemma, in mathcomp.fingroup.quotient]
quotient_isog [lemma, in mathcomp.fingroup.quotient]
quotient_isom [lemma, in mathcomp.fingroup.quotient]
quotient_subnormG [lemma, in mathcomp.fingroup.quotient]
quotient_normG [lemma, in mathcomp.fingroup.quotient]
quotient_subcent [lemma, in mathcomp.fingroup.quotient]
quotient_abelian [lemma, in mathcomp.fingroup.quotient]
quotient_cents [lemma, in mathcomp.fingroup.quotient]
quotient_cent [lemma, in mathcomp.fingroup.quotient]
quotient_subcent1 [lemma, in mathcomp.fingroup.quotient]
quotient_cent1s [lemma, in mathcomp.fingroup.quotient]
quotient_cent1 [lemma, in mathcomp.fingroup.quotient]
quotient_normal [lemma, in mathcomp.fingroup.quotient]
quotient_subnorm [lemma, in mathcomp.fingroup.quotient]
quotient_norms [lemma, in mathcomp.fingroup.quotient]
quotient_norm [lemma, in mathcomp.fingroup.quotient]
quotient_gen [lemma, in mathcomp.fingroup.quotient]
quotient_neq1 [lemma, in mathcomp.fingroup.quotient]
quotient_inj [lemma, in mathcomp.fingroup.quotient]
quotient_injG [lemma, in mathcomp.fingroup.quotient]
quotient_sub1 [lemma, in mathcomp.fingroup.quotient]
quotient_proper [lemma, in mathcomp.fingroup.quotient]
quotient_class [lemma, in mathcomp.fingroup.quotient]
quotient_homg [lemma, in mathcomp.fingroup.quotient]
quotient_set1 [lemma, in mathcomp.fingroup.quotient]
quotient_setIpre [lemma, in mathcomp.fingroup.quotient]
quotient_group [definition, in mathcomp.fingroup.quotient]
quotient_der [lemma, in mathcomp.solvable.commutator]
quotient_cents2r [lemma, in mathcomp.solvable.commutator]
quotient_cents2 [lemma, in mathcomp.solvable.commutator]
quotient_of_section [definition, in mathcomp.solvable.jordanholder]
quotient_astabQ [lemma, in mathcomp.fingroup.action]
quotient_groupAction [definition, in mathcomp.fingroup.action]
quotient_action [definition, in mathcomp.fingroup.action]
quotient_cfker_mod [lemma, in mathcomp.character.classfun]
quotient_pseries_cat [lemma, in mathcomp.solvable.pgroup]
quotient_pseries2 [lemma, in mathcomp.solvable.pgroup]
quotient_pseries [lemma, in mathcomp.solvable.pgroup]
quotient_pcore_mod [lemma, in mathcomp.solvable.pgroup]
quotient_odd [lemma, in mathcomp.solvable.pgroup]
quotient_pHall [lemma, in mathcomp.solvable.pgroup]
quotient_pgroup [lemma, in mathcomp.solvable.pgroup]
quotient_splitting_field [lemma, in mathcomp.character.mxrepresentation]
quotient_coprime_dprod [lemma, in mathcomp.fingroup.gproduct]
quotient_cprod [lemma, in mathcomp.fingroup.gproduct]
quotient_coprime_sdprod [lemma, in mathcomp.fingroup.gproduct]
quotient_pprod [lemma, in mathcomp.fingroup.gproduct]
quotient_sdprodr_isog [lemma, in mathcomp.fingroup.gproduct]
quotient_sdprodr_isom [lemma, in mathcomp.fingroup.gproduct]
quotient_p_rank_abelian [lemma, in mathcomp.solvable.abelian]
quotient_rank_abelian [lemma, in mathcomp.solvable.abelian]
quotient_grank [lemma, in mathcomp.solvable.abelian]
quotient_pnElem [lemma, in mathcomp.solvable.abelian]
quotient_pElem [lemma, in mathcomp.solvable.abelian]
quotient_abelem [lemma, in mathcomp.solvable.abelian]
quotient_Ldiv [lemma, in mathcomp.solvable.abelian]
quotient_LdivT [lemma, in mathcomp.solvable.abelian]
quotient_simple [lemma, in mathcomp.solvable.gseries]
quotient_maximal_eq [lemma, in mathcomp.solvable.gseries]
quotient_maximal [lemma, in mathcomp.solvable.gseries]
quotient_subnormal [lemma, in mathcomp.solvable.gseries]
quotient_generator [lemma, in mathcomp.solvable.cyclic]
quotient_cyclic [lemma, in mathcomp.solvable.cyclic]
quotient_cycle [lemma, in mathcomp.solvable.cyclic]
quotient_TI_subcent [lemma, in mathcomp.solvable.hall]
quotient_Phi [lemma, in mathcomp.solvable.maximal]
quotient_sol [lemma, in mathcomp.solvable.nilpotent]
quotient_center_nil [lemma, in mathcomp.solvable.nilpotent]
quotient_nil [lemma, in mathcomp.solvable.nilpotent]
quotient_ucn_add [lemma, in mathcomp.solvable.nilpotent]
Quotient.add [definition, in mathcomp.algebra.ring_quotient]
Quotient.addNq [lemma, in mathcomp.algebra.ring_quotient]
Quotient.addqA [lemma, in mathcomp.algebra.ring_quotient]
Quotient.addqC [lemma, in mathcomp.algebra.ring_quotient]
Quotient.add0q [lemma, in mathcomp.algebra.ring_quotient]
Quotient.equiv [definition, in mathcomp.algebra.ring_quotient]
Quotient.equivE [lemma, in mathcomp.algebra.ring_quotient]
Quotient.equiv_encModRel [definition, in mathcomp.algebra.ring_quotient]
Quotient.equiv_equiv [definition, in mathcomp.algebra.ring_quotient]
Quotient.equiv_is_equiv [lemma, in mathcomp.algebra.ring_quotient]
Quotient.Exports [module, in mathcomp.algebra.ring_quotient]
Quotient.I [abbreviation, in mathcomp.algebra.ring_quotient]
Quotient.idealrBE [lemma, in mathcomp.algebra.ring_quotient]
Quotient.idealrDE [lemma, in mathcomp.algebra.ring_quotient]
Quotient.IDomainQuotient [section, in mathcomp.algebra.ring_quotient]
Quotient.IDomainQuotient.I [variable, in mathcomp.algebra.ring_quotient]
Quotient.IDomainQuotient.R [variable, in mathcomp.algebra.ring_quotient]
Quotient.mul [definition, in mathcomp.algebra.ring_quotient]
Quotient.mulqA [lemma, in mathcomp.algebra.ring_quotient]
Quotient.mulqC [lemma, in mathcomp.algebra.ring_quotient]
Quotient.mulq_addl [lemma, in mathcomp.algebra.ring_quotient]
Quotient.mul1q [lemma, in mathcomp.algebra.ring_quotient]
Quotient.nonzero1q [lemma, in mathcomp.algebra.ring_quotient]
Quotient.one [definition, in mathcomp.algebra.ring_quotient]
Quotient.opp [definition, in mathcomp.algebra.ring_quotient]
Quotient.pi_mul_morph [definition, in mathcomp.algebra.ring_quotient]
Quotient.pi_mul [lemma, in mathcomp.algebra.ring_quotient]
Quotient.pi_one_morph [definition, in mathcomp.algebra.ring_quotient]
Quotient.pi_add_morph [definition, in mathcomp.algebra.ring_quotient]
Quotient.pi_add [lemma, in mathcomp.algebra.ring_quotient]
Quotient.pi_opp_morph [definition, in mathcomp.algebra.ring_quotient]
Quotient.pi_opp [lemma, in mathcomp.algebra.ring_quotient]
Quotient.pi_zero_morph [definition, in mathcomp.algebra.ring_quotient]
Quotient.quot [definition, in mathcomp.algebra.ring_quotient]
Quotient.RingQuotient [section, in mathcomp.algebra.ring_quotient]
Quotient.RingQuotient.idealI [variable, in mathcomp.algebra.ring_quotient]
Quotient.RingQuotient.R [variable, in mathcomp.algebra.ring_quotient]
Quotient.rquot_IdomainAxiom [lemma, in mathcomp.algebra.ring_quotient]
Quotient.zero [definition, in mathcomp.algebra.ring_quotient]
Quotient.ZmodQuotient [section, in mathcomp.algebra.ring_quotient]
Quotient.ZmodQuotient.I [variable, in mathcomp.algebra.ring_quotient]
Quotient.ZmodQuotient.R [variable, in mathcomp.algebra.ring_quotient]
{ quot _ } (type_scope) [notation, in mathcomp.algebra.ring_quotient]
quotient0 [lemma, in mathcomp.fingroup.quotient]
Quotient1 [section, in mathcomp.fingroup.quotient]
quotient1 [lemma, in mathcomp.fingroup.quotient]
quotient1_isog [lemma, in mathcomp.fingroup.quotient]
quotient1_isom [lemma, in mathcomp.fingroup.quotient]
Quotient1.A [variable, in mathcomp.fingroup.quotient]
Quotient1.gT [variable, in mathcomp.fingroup.quotient]
quotm [definition, in mathcomp.fingroup.quotient]
quotmE [lemma, in mathcomp.fingroup.quotient]
quotm_morphism [definition, in mathcomp.fingroup.quotient]
quotm_ker_proof [lemma, in mathcomp.fingroup.quotient]
quotm_dom_proof [lemma, in mathcomp.fingroup.quotient]
quotP [lemma, in mathcomp.ssreflect.generic_quotient]
QuotSubType [module, in mathcomp.ssreflect.generic_quotient]
QuotSubType.Exports [module, in mathcomp.ssreflect.generic_quotient]
QuotSubType.qreprK [lemma, in mathcomp.ssreflect.generic_quotient]
QuotSubType.QuotSubType [section, in mathcomp.ssreflect.generic_quotient]
QuotSubType.QuotSubType.qT [variable, in mathcomp.ssreflect.generic_quotient]
QuotSubType.QuotSubType.T [variable, in mathcomp.ssreflect.generic_quotient]
QuotSubType.reprP [lemma, in mathcomp.ssreflect.generic_quotient]
QuotSubType.sortPx [lemma, in mathcomp.ssreflect.generic_quotient]
QuotSubType.sort_Sub [lemma, in mathcomp.ssreflect.generic_quotient]
QuotSubType.Sub [definition, in mathcomp.ssreflect.generic_quotient]
QuotTypeTheory [section, in mathcomp.ssreflect.generic_quotient]
QuotTypeTheory.qT [variable, in mathcomp.ssreflect.generic_quotient]
QuotTypeTheory.T [variable, in mathcomp.ssreflect.generic_quotient]
quotW [lemma, in mathcomp.ssreflect.generic_quotient]
quot_type [abbreviation, in mathcomp.ssreflect.generic_quotient]
quot_type_of [definition, in mathcomp.ssreflect.generic_quotient]
quot_pi_subdef:4 [binder, in mathcomp.ssreflect.generic_quotient]
quo_mx_irr [lemma, in mathcomp.character.mxrepresentation]
quo_mx_quotient [lemma, in mathcomp.character.mxrepresentation]
quo_repr_coset [lemma, in mathcomp.character.mxrepresentation]
quo_repr [definition, in mathcomp.character.mxrepresentation]
quo_mx_repr [lemma, in mathcomp.character.mxrepresentation]
quo_mx_coset [lemma, in mathcomp.character.mxrepresentation]
quo_mx [definition, in mathcomp.character.mxrepresentation]
quo_IirrKeq [lemma, in mathcomp.character.character]
quo_IirrK [lemma, in mathcomp.character.character]
quo_Iirr_eq0 [lemma, in mathcomp.character.character]
quo_IirrE [lemma, in mathcomp.character.character]
quo_Iirr0 [lemma, in mathcomp.character.character]
quo_Iirr [definition, in mathcomp.character.character]
quo:335 [binder, in mathcomp.algebra.polydiv]
Qxz:125 [binder, in mathcomp.field.algebraics_fundamentals]
Qxz:129 [binder, in mathcomp.field.algebraics_fundamentals]
qX_expK [lemma, in mathcomp.field.qfpoly]
qX_exp_inj [lemma, in mathcomp.field.qfpoly]
qX_exp_neq0 [lemma, in mathcomp.field.qfpoly]
qX_order_dvd [lemma, in mathcomp.field.qfpoly]
qX_order_card [lemma, in mathcomp.field.qfpoly]
qX_in_unit [lemma, in mathcomp.field.qfpoly]
qX_neq0 [lemma, in mathcomp.field.qfpoly]
Qz1:69 [binder, in mathcomp.field.algnum]
Qz2:70 [binder, in mathcomp.field.algnum]
Qz:62 [binder, in mathcomp.field.algnum]
Qz:64 [binder, in mathcomp.field.algnum]
Qz:70 [binder, in mathcomp.field.algebraics_fundamentals]
q_k:67 [binder, in mathcomp.field.algC]
q_:3522 [binder, in mathcomp.algebra.matrix]
q_:3507 [binder, in mathcomp.algebra.matrix]
q_:3307 [binder, in mathcomp.algebra.matrix]
q_:3249 [binder, in mathcomp.algebra.matrix]
q_:3165 [binder, in mathcomp.algebra.matrix]
q_:3058 [binder, in mathcomp.algebra.matrix]
q_:2989 [binder, in mathcomp.algebra.matrix]
q_:2961 [binder, in mathcomp.algebra.matrix]
q_:2950 [binder, in mathcomp.algebra.matrix]
q_:2938 [binder, in mathcomp.algebra.matrix]
q_:2926 [binder, in mathcomp.algebra.matrix]
q_:2864 [binder, in mathcomp.algebra.matrix]
q_:2679 [binder, in mathcomp.algebra.matrix]
q_unitP:398 [binder, in mathcomp.field.closed_field]
q1:108 [binder, in mathcomp.algebra.qpoly]
q1:113 [binder, in mathcomp.algebra.polydiv]
q1:119 [binder, in mathcomp.algebra.qpoly]
q1:120 [binder, in mathcomp.algebra.polydiv]
q1:168 [binder, in mathcomp.algebra.polydiv]
q1:230 [binder, in mathcomp.field.closed_field]
q1:234 [binder, in mathcomp.field.closed_field]
q1:253 [binder, in mathcomp.field.algnum]
q1:262 [binder, in mathcomp.field.algnum]
q1:569 [binder, in mathcomp.algebra.polydiv]
q1:67 [binder, in mathcomp.field.qfpoly]
q1:82 [binder, in mathcomp.field.qfpoly]
q1:943 [binder, in mathcomp.algebra.polydiv]
q1:950 [binder, in mathcomp.algebra.polydiv]
q2:109 [binder, in mathcomp.algebra.qpoly]
q2:120 [binder, in mathcomp.algebra.qpoly]
q2:256 [binder, in mathcomp.field.galois]
q2:570 [binder, in mathcomp.algebra.polydiv]
q2:68 [binder, in mathcomp.field.qfpoly]
q2:83 [binder, in mathcomp.field.qfpoly]
q2:944 [binder, in mathcomp.algebra.polydiv]
q2:951 [binder, in mathcomp.algebra.polydiv]
Q8_extraspecial [lemma, in mathcomp.solvable.extraspecial]
q:1 [binder, in mathcomp.ssreflect.prime]
q:10 [binder, in mathcomp.algebra.polyXY]
q:100 [binder, in mathcomp.algebra.polydiv]
q:100 [binder, in mathcomp.field.closed_field]
q:1002 [binder, in mathcomp.algebra.polydiv]
q:1007 [binder, in mathcomp.algebra.polydiv]
Q:101 [binder, in mathcomp.ssreflect.generic_quotient]
q:1011 [binder, in mathcomp.algebra.polydiv]
q:1014 [binder, in mathcomp.algebra.polydiv]
q:1017 [binder, in mathcomp.algebra.polydiv]
q:1019 [binder, in mathcomp.algebra.polydiv]
q:102 [binder, in mathcomp.algebra.polydiv]
q:102 [binder, in mathcomp.field.algC]
q:102 [binder, in mathcomp.algebra.poly]
q:102 [binder, in mathcomp.algebra.qpoly]
q:1021 [binder, in mathcomp.algebra.polydiv]
q:1023 [binder, in mathcomp.algebra.polydiv]
q:1025 [binder, in mathcomp.algebra.polydiv]
q:1027 [binder, in mathcomp.algebra.polydiv]
q:1033 [binder, in mathcomp.algebra.polydiv]
q:1038 [binder, in mathcomp.algebra.polydiv]
q:104 [binder, in mathcomp.algebra.poly]
q:1041 [binder, in mathcomp.algebra.polydiv]
q:1044 [binder, in mathcomp.algebra.polydiv]
q:1047 [binder, in mathcomp.algebra.polydiv]
q:1050 [binder, in mathcomp.algebra.polydiv]
q:1053 [binder, in mathcomp.algebra.polydiv]
q:106 [binder, in mathcomp.field.closed_field]
q:106 [binder, in mathcomp.algebra.poly]
q:1066 [binder, in mathcomp.algebra.polydiv]
q:1067 [binder, in mathcomp.algebra.poly]
q:1068 [binder, in mathcomp.algebra.polydiv]
q:107 [binder, in mathcomp.algebra.polydiv]
q:1070 [binder, in mathcomp.algebra.polydiv]
q:1072 [binder, in mathcomp.algebra.polydiv]
q:1074 [binder, in mathcomp.algebra.polydiv]
q:1076 [binder, in mathcomp.algebra.polydiv]
q:1078 [binder, in mathcomp.algebra.polydiv]
q:1080 [binder, in mathcomp.algebra.polydiv]
q:1082 [binder, in mathcomp.algebra.polydiv]
q:1085 [binder, in mathcomp.algebra.polydiv]
q:1088 [binder, in mathcomp.algebra.polydiv]
q:1091 [binder, in mathcomp.algebra.polydiv]
q:1094 [binder, in mathcomp.algebra.poly]
q:1095 [binder, in mathcomp.algebra.poly]
q:1097 [binder, in mathcomp.algebra.poly]
q:11 [binder, in mathcomp.ssreflect.div]
q:1100 [binder, in mathcomp.algebra.poly]
q:1103 [binder, in mathcomp.algebra.poly]
q:1106 [binder, in mathcomp.algebra.poly]
q:1109 [binder, in mathcomp.algebra.poly]
q:1114 [binder, in mathcomp.algebra.poly]
q:1116 [binder, in mathcomp.algebra.poly]
Q:112 [binder, in mathcomp.ssreflect.generic_quotient]
q:112 [binder, in mathcomp.character.mxabelem]
q:112 [binder, in mathcomp.algebra.poly]
q:1120 [binder, in mathcomp.algebra.poly]
q:1125 [binder, in mathcomp.algebra.poly]
q:1138 [binder, in mathcomp.algebra.poly]
q:114 [binder, in mathcomp.field.closed_field]
q:115 [binder, in mathcomp.character.mxabelem]
q:116 [binder, in mathcomp.algebra.polydiv]
q:1170 [binder, in mathcomp.algebra.poly]
q:118 [binder, in mathcomp.algebra.poly]
q:1183 [binder, in mathcomp.algebra.mxalgebra]
q:119 [binder, in mathcomp.character.mxabelem]
Q:119 [binder, in mathcomp.solvable.gseries]
q:1199 [binder, in mathcomp.algebra.poly]
q:12 [binder, in mathcomp.algebra.polyXY]
Q:120 [binder, in mathcomp.algebra.ring_quotient]
q:120 [binder, in mathcomp.field.finfield]
q:1201 [binder, in mathcomp.algebra.poly]
q:1204 [binder, in mathcomp.algebra.poly]
q:1205 [binder, in mathcomp.ssreflect.ssrnat]
q:1206 [binder, in mathcomp.algebra.poly]
q:1207 [binder, in mathcomp.ssreflect.ssrnat]
q:1208 [binder, in mathcomp.algebra.poly]
q:121 [binder, in mathcomp.field.closed_field]
Q:121 [binder, in mathcomp.solvable.gseries]
Q:122 [binder, in mathcomp.ssreflect.choice]
q:122 [binder, in mathcomp.character.mxabelem]
q:1241 [binder, in mathcomp.algebra.poly]
q:126 [binder, in mathcomp.ssreflect.prime]
q:129 [binder, in mathcomp.algebra.polydiv]
q:1317 [binder, in mathcomp.algebra.poly]
q:132 [binder, in mathcomp.algebra.qpoly]
q:1325 [binder, in mathcomp.algebra.poly]
q:133 [binder, in mathcomp.algebra.polydiv]
Q:1335 [binder, in mathcomp.ssreflect.finset]
Q:1337 [binder, in mathcomp.ssreflect.finset]
Q:1339 [binder, in mathcomp.ssreflect.finset]
q:135 [binder, in mathcomp.algebra.polydiv]
q:135 [binder, in mathcomp.field.closed_field]
q:135 [binder, in mathcomp.algebra.qpoly]
Q:1367 [binder, in mathcomp.ssreflect.bigop]
Q:1378 [binder, in mathcomp.ssreflect.bigop]
q:138 [binder, in mathcomp.algebra.polydiv]
q:142 [binder, in mathcomp.algebra.polydiv]
Q:1437 [binder, in mathcomp.ssreflect.order]
Q:1446 [binder, in mathcomp.ssreflect.order]
q:145 [binder, in mathcomp.algebra.poly]
Q:1455 [binder, in mathcomp.ssreflect.order]
q:146 [binder, in mathcomp.algebra.polydiv]
Q:1464 [binder, in mathcomp.ssreflect.order]
Q:147 [binder, in mathcomp.solvable.hall]
q:15 [binder, in mathcomp.algebra.polydiv]
q:150 [binder, in mathcomp.algebra.polydiv]
q:151 [binder, in mathcomp.algebra.poly]
q:152 [binder, in mathcomp.algebra.archimedean]
q:152 [binder, in mathcomp.field.closed_field]
q:153 [binder, in mathcomp.algebra.polydiv]
q:153 [binder, in mathcomp.field.falgebra]
q:1535 [binder, in mathcomp.algebra.matrix]
Q:1538 [binder, in mathcomp.ssreflect.bigop]
q:154 [binder, in mathcomp.algebra.qpoly]
Q:1554 [binder, in mathcomp.ssreflect.finset]
q:156 [binder, in mathcomp.algebra.qpoly]
Q:1563 [binder, in mathcomp.ssreflect.bigop]
q:157 [binder, in mathcomp.algebra.poly]
Q:1583 [binder, in mathcomp.ssreflect.bigop]
q:159 [binder, in mathcomp.algebra.poly]
q:16 [binder, in mathcomp.algebra.poly]
Q:1601 [binder, in mathcomp.ssreflect.bigop]
q:161 [binder, in mathcomp.field.closed_field]
q:161 [binder, in mathcomp.algebra.poly]
Q:1629 [binder, in mathcomp.ssreflect.bigop]
q:163 [binder, in mathcomp.algebra.poly]
q:164 [binder, in mathcomp.algebra.qpoly]
q:165 [binder, in mathcomp.algebra.intdiv]
Q:1652 [binder, in mathcomp.ssreflect.bigop]
q:167 [binder, in mathcomp.algebra.polydiv]
q:167 [binder, in mathcomp.algebra.qpoly]
Q:1671 [binder, in mathcomp.ssreflect.bigop]
Q:1694 [binder, in mathcomp.ssreflect.bigop]
q:17 [binder, in mathcomp.ssreflect.div]
q:17 [binder, in mathcomp.algebra.polydiv]
q:17 [binder, in mathcomp.algebra.polyXY]
q:170 [binder, in mathcomp.field.closed_field]
Q:170 [binder, in mathcomp.solvable.sylow]
q:172 [binder, in mathcomp.field.algebraics_fundamentals]
Q:172 [binder, in mathcomp.ssreflect.fintype]
q:175 [binder, in mathcomp.field.closed_field]
q:177 [binder, in mathcomp.algebra.qpoly]
q:178 [binder, in mathcomp.algebra.mxpoly]
q:1780 [binder, in mathcomp.algebra.matrix]
Q:1783 [binder, in mathcomp.ssreflect.bigop]
Q:1794 [binder, in mathcomp.ssreflect.bigop]
q:18 [binder, in mathcomp.algebra.polyXY]
q:180 [binder, in mathcomp.algebra.mxpoly]
q:181 [binder, in mathcomp.algebra.qpoly]
q:182 [binder, in mathcomp.algebra.polydiv]
q:182 [binder, in mathcomp.field.algebraics_fundamentals]
q:182 [binder, in mathcomp.algebra.mxpoly]
q:1825 [binder, in mathcomp.algebra.ssrnum]
q:183 [binder, in mathcomp.field.algebraics_fundamentals]
q:186 [binder, in mathcomp.algebra.polydiv]
q:186 [binder, in mathcomp.field.closed_field]
q:19 [binder, in mathcomp.algebra.polydiv]
q:19 [binder, in mathcomp.algebra.polyXY]
q:19 [binder, in mathcomp.algebra.qpoly]
q:190 [binder, in mathcomp.field.closed_field]
q:191 [binder, in mathcomp.field.algebraics_fundamentals]
q:193 [binder, in mathcomp.field.algebraics_fundamentals]
q:193 [binder, in mathcomp.field.closed_field]
q:195 [binder, in mathcomp.algebra.poly]
q:196 [binder, in mathcomp.field.closed_field]
q:197 [binder, in mathcomp.field.algebraics_fundamentals]
q:199 [binder, in mathcomp.field.closed_field]
q:2 [binder, in mathcomp.algebra.polydiv]
q:20 [binder, in mathcomp.algebra.polyXY]
q:201 [binder, in mathcomp.algebra.polydiv]
q:202 [binder, in mathcomp.field.closed_field]
q:2031 [binder, in mathcomp.algebra.matrix]
q:2038 [binder, in mathcomp.algebra.matrix]
q:209 [binder, in mathcomp.algebra.polydiv]
q:21 [binder, in mathcomp.algebra.polydiv]
q:21 [binder, in mathcomp.algebra.polyXY]
q:210 [binder, in mathcomp.ssreflect.prime]
Q:2121 [binder, in mathcomp.ssreflect.bigop]
Q:2157 [binder, in mathcomp.ssreflect.bigop]
q:218 [binder, in mathcomp.ssreflect.fingraph]
q:219 [binder, in mathcomp.algebra.polydiv]
q:22 [binder, in mathcomp.field.separable]
q:220 [binder, in mathcomp.ssreflect.fingraph]
Q:2207 [binder, in mathcomp.ssreflect.bigop]
q:221 [binder, in mathcomp.algebra.polydiv]
q:222 [binder, in mathcomp.field.closed_field]
q:222 [binder, in mathcomp.ssreflect.fingraph]
Q:2223 [binder, in mathcomp.ssreflect.bigop]
q:223 [binder, in mathcomp.algebra.polydiv]
Q:2237 [binder, in mathcomp.ssreflect.bigop]
q:225 [binder, in mathcomp.algebra.polydiv]
q:226 [binder, in mathcomp.field.closed_field]
Q:2265 [binder, in mathcomp.ssreflect.bigop]
q:227 [binder, in mathcomp.algebra.polydiv]
q:228 [binder, in mathcomp.field.closed_field]
Q:2287 [binder, in mathcomp.ssreflect.bigop]
q:229 [binder, in mathcomp.algebra.polydiv]
q:23 [binder, in mathcomp.algebra.polydiv]
q:23 [binder, in mathcomp.algebra.mxpoly]
q:23 [binder, in mathcomp.field.qfpoly]
Q:2306 [binder, in mathcomp.ssreflect.bigop]
q:231 [binder, in mathcomp.field.algC]
q:232 [binder, in mathcomp.algebra.polydiv]
Q:2328 [binder, in mathcomp.ssreflect.bigop]
q:234 [binder, in mathcomp.algebra.polydiv]
q:236 [binder, in mathcomp.algebra.polydiv]
q:238 [binder, in mathcomp.algebra.polydiv]
q:24 [binder, in mathcomp.field.separable]
q:240 [binder, in mathcomp.algebra.polydiv]
q:241 [binder, in mathcomp.field.closed_field]
q:242 [binder, in mathcomp.algebra.polydiv]
q:243 [binder, in mathcomp.ssreflect.seq]
q:243 [binder, in mathcomp.algebra.poly]
q:244 [binder, in mathcomp.algebra.polydiv]
q:244 [binder, in mathcomp.field.closed_field]
q:245 [binder, in mathcomp.field.galois]
q:245 [binder, in mathcomp.algebra.poly]
Q:2480 [binder, in mathcomp.ssreflect.seq]
Q:2498 [binder, in mathcomp.ssreflect.seq]
q:25 [binder, in mathcomp.algebra.polydiv]
q:250 [binder, in mathcomp.algebra.polydiv]
q:252 [binder, in mathcomp.algebra.polydiv]
q:253 [binder, in mathcomp.algebra.poly]
q:257 [binder, in mathcomp.algebra.polydiv]
q:257 [binder, in mathcomp.field.algC]
q:258 [binder, in mathcomp.algebra.intdiv]
q:258 [binder, in mathcomp.algebra.mxpoly]
q:259 [binder, in mathcomp.field.closed_field]
q:26 [binder, in mathcomp.field.separable]
q:26 [binder, in mathcomp.ssreflect.path]
q:260 [binder, in mathcomp.algebra.polydiv]
q:261 [binder, in mathcomp.algebra.polydiv]
Q:2614 [binder, in mathcomp.ssreflect.bigop]
Q:2656 [binder, in mathcomp.ssreflect.bigop]
q:2667 [binder, in mathcomp.algebra.matrix]
q:267 [binder, in mathcomp.algebra.polydiv]
Q:2674 [binder, in mathcomp.ssreflect.bigop]
q:2677 [binder, in mathcomp.algebra.matrix]
Q:2693 [binder, in mathcomp.ssreflect.bigop]
Q:27 [binder, in mathcomp.algebra.ring_quotient]
q:271 [binder, in mathcomp.field.closed_field]
q:272 [binder, in mathcomp.algebra.polydiv]
q:274 [binder, in mathcomp.algebra.polydiv]
Q:2759 [binder, in mathcomp.ssreflect.seq]
q:276 [binder, in mathcomp.field.closed_field]
q:277 [binder, in mathcomp.field.closed_field]
q:279 [binder, in mathcomp.algebra.polydiv]
q:281 [binder, in mathcomp.algebra.polydiv]
q:284 [binder, in mathcomp.field.closed_field]
q:2862 [binder, in mathcomp.algebra.matrix]
q:287 [binder, in mathcomp.field.closed_field]
q:289 [binder, in mathcomp.algebra.polydiv]
q:289 [binder, in mathcomp.field.closed_field]
q:29 [binder, in mathcomp.algebra.polydiv]
q:2924 [binder, in mathcomp.algebra.matrix]
q:293 [binder, in mathcomp.algebra.polydiv]
q:2936 [binder, in mathcomp.algebra.matrix]
q:294 [binder, in mathcomp.field.closed_field]
q:2948 [binder, in mathcomp.algebra.matrix]
q:2960 [binder, in mathcomp.algebra.matrix]
q:297 [binder, in mathcomp.algebra.mxpoly]
q:2988 [binder, in mathcomp.algebra.matrix]
q:299 [binder, in mathcomp.ssreflect.div]
q:299 [binder, in mathcomp.algebra.polydiv]
q:3 [binder, in mathcomp.ssreflect.div]
q:301 [binder, in mathcomp.algebra.polydiv]
q:301 [binder, in mathcomp.algebra.mxpoly]
q:301 [binder, in mathcomp.field.closed_field]
q:302 [binder, in mathcomp.ssreflect.div]
q:305 [binder, in mathcomp.ssreflect.div]
q:305 [binder, in mathcomp.algebra.polydiv]
q:309 [binder, in mathcomp.algebra.polydiv]
q:31 [binder, in mathcomp.algebra.polydiv]
q:311 [binder, in mathcomp.algebra.polydiv]
q:311 [binder, in mathcomp.field.fieldext]
q:312 [binder, in mathcomp.field.fieldext]
q:313 [binder, in mathcomp.algebra.polydiv]
q:319 [binder, in mathcomp.field.fieldext]
Q:32 [binder, in mathcomp.ssreflect.ssrbool]
q:320 [binder, in mathcomp.algebra.polydiv]
q:321 [binder, in mathcomp.field.fieldext]
q:324 [binder, in mathcomp.algebra.polydiv]
q:3247 [binder, in mathcomp.algebra.matrix]
q:326 [binder, in mathcomp.algebra.polydiv]
q:326 [binder, in mathcomp.field.fieldext]
Q:327 [binder, in mathcomp.solvable.pgroup]
q:328 [binder, in mathcomp.algebra.polydiv]
Q:328 [binder, in mathcomp.solvable.pgroup]
q:329 [binder, in mathcomp.field.closed_field]
Q:329 [binder, in mathcomp.solvable.pgroup]
q:330 [binder, in mathcomp.field.closed_field]
Q:330 [binder, in mathcomp.solvable.pgroup]
q:3304 [binder, in mathcomp.algebra.matrix]
q:331 [binder, in mathcomp.algebra.polydiv]
q:331 [binder, in mathcomp.field.closed_field]
Q:331 [binder, in mathcomp.solvable.pgroup]
q:331 [binder, in mathcomp.algebra.poly]
q:333 [binder, in mathcomp.algebra.polydiv]
q:333 [binder, in mathcomp.algebra.poly]
q:335 [binder, in mathcomp.algebra.poly]
q:336 [binder, in mathcomp.algebra.polydiv]
q:337 [binder, in mathcomp.algebra.poly]
q:339 [binder, in mathcomp.algebra.poly]
q:340 [binder, in mathcomp.algebra.polydiv]
q:341 [binder, in mathcomp.algebra.poly]
q:347 [binder, in mathcomp.field.fieldext]
q:35 [binder, in mathcomp.algebra.polydiv]
q:35 [binder, in mathcomp.solvable.extremal]
q:3505 [binder, in mathcomp.algebra.matrix]
q:352 [binder, in mathcomp.field.fieldext]
q:3520 [binder, in mathcomp.algebra.matrix]
q:353 [binder, in mathcomp.field.fieldext]
q:36 [binder, in mathcomp.field.algebraics_fundamentals]
q:368 [binder, in mathcomp.field.fieldext]
q:37 [binder, in mathcomp.algebra.polydiv]
q:370 [binder, in mathcomp.field.fieldext]
q:371 [binder, in mathcomp.field.fieldext]
q:376 [binder, in mathcomp.algebra.polydiv]
q:378 [binder, in mathcomp.algebra.polydiv]
q:379 [binder, in mathcomp.solvable.extremal]
q:38 [binder, in mathcomp.ssreflect.div]
q:381 [binder, in mathcomp.algebra.polydiv]
q:381 [binder, in mathcomp.field.closed_field]
q:382 [binder, in mathcomp.algebra.poly]
q:383 [binder, in mathcomp.field.algnum]
q:384 [binder, in mathcomp.algebra.polydiv]
q:384 [binder, in mathcomp.field.algnum]
q:385 [binder, in mathcomp.field.algnum]
q:387 [binder, in mathcomp.algebra.polydiv]
q:388 [binder, in mathcomp.algebra.intdiv]
q:389 [binder, in mathcomp.field.closed_field]
q:39 [binder, in mathcomp.algebra.polydiv]
q:396 [binder, in mathcomp.field.closed_field]
q:398 [binder, in mathcomp.algebra.polydiv]
q:4 [binder, in mathcomp.ssreflect.choice]
q:401 [binder, in mathcomp.algebra.intdiv]
q:401 [binder, in mathcomp.algebra.polydiv]
q:405 [binder, in mathcomp.algebra.mxpoly]
q:406 [binder, in mathcomp.algebra.intdiv]
q:408 [binder, in mathcomp.algebra.intdiv]
q:411 [binder, in mathcomp.algebra.intdiv]
q:413 [binder, in mathcomp.algebra.intdiv]
q:417 [binder, in mathcomp.algebra.intdiv]
q:42 [binder, in mathcomp.algebra.intdiv]
q:42 [binder, in mathcomp.algebra.polydiv]
Q:42 [binder, in mathcomp.solvable.sylow]
q:424 [binder, in mathcomp.algebra.intdiv]
q:426 [binder, in mathcomp.algebra.intdiv]
q:428 [binder, in mathcomp.algebra.polydiv]
q:430 [binder, in mathcomp.field.closed_field]
q:432 [binder, in mathcomp.algebra.poly]
q:433 [binder, in mathcomp.algebra.polydiv]
q:437 [binder, in mathcomp.algebra.polydiv]
q:438 [binder, in mathcomp.algebra.polydiv]
q:460 [binder, in mathcomp.algebra.polydiv]
q:463 [binder, in mathcomp.algebra.polydiv]
q:466 [binder, in mathcomp.algebra.polydiv]
q:467 [binder, in mathcomp.algebra.polydiv]
q:467 [binder, in mathcomp.algebra.poly]
q:471 [binder, in mathcomp.algebra.polydiv]
q:473 [binder, in mathcomp.algebra.poly]
Q:474 [binder, in mathcomp.ssreflect.ssrnat]
q:476 [binder, in mathcomp.algebra.poly]
q:477 [binder, in mathcomp.algebra.polydiv]
Q:478 [binder, in mathcomp.ssreflect.ssrnat]
q:479 [binder, in mathcomp.algebra.polydiv]
q:48 [binder, in mathcomp.solvable.alt]
Q:48 [binder, in mathcomp.algebra.ring_quotient]
q:481 [binder, in mathcomp.algebra.polydiv]
q:483 [binder, in mathcomp.algebra.polydiv]
q:486 [binder, in mathcomp.algebra.polydiv]
q:49 [binder, in mathcomp.solvable.alt]
q:49 [binder, in mathcomp.field.fieldext]
q:49 [binder, in mathcomp.algebra.mxpoly]
q:490 [binder, in mathcomp.algebra.polydiv]
q:4945 [binder, in mathcomp.ssreflect.order]
q:4947 [binder, in mathcomp.ssreflect.order]
q:4958 [binder, in mathcomp.ssreflect.order]
q:4960 [binder, in mathcomp.ssreflect.order]
q:499 [binder, in mathcomp.algebra.polydiv]
q:50 [binder, in mathcomp.solvable.alt]
q:50 [binder, in mathcomp.field.separable]
Q:50 [binder, in mathcomp.solvable.sylow]
q:50 [binder, in mathcomp.algebra.qpoly]
q:509 [binder, in mathcomp.algebra.polydiv]
q:51 [binder, in mathcomp.algebra.polydiv]
q:51 [binder, in mathcomp.field.separable]
q:51 [binder, in mathcomp.algebra.qpoly]
q:513 [binder, in mathcomp.algebra.polydiv]
q:515 [binder, in mathcomp.algebra.polydiv]
q:515 [binder, in mathcomp.algebra.poly]
q:517 [binder, in mathcomp.algebra.polydiv]
q:519 [binder, in mathcomp.algebra.polydiv]
q:52 [binder, in mathcomp.algebra.qpoly]
q:521 [binder, in mathcomp.algebra.polydiv]
q:521 [binder, in mathcomp.algebra.poly]
q:522 [binder, in mathcomp.algebra.poly]
q:526 [binder, in mathcomp.algebra.polydiv]
q:530 [binder, in mathcomp.algebra.polydiv]
q:54 [binder, in mathcomp.field.fieldext]
Q:548 [binder, in mathcomp.ssreflect.bigop]
Q:55 [binder, in mathcomp.solvable.sylow]
q:558 [binder, in mathcomp.algebra.polydiv]
q:56 [binder, in mathcomp.algebra.poly]
q:562 [binder, in mathcomp.algebra.polydiv]
q:566 [binder, in mathcomp.algebra.polydiv]
q:57 [binder, in mathcomp.algebra.polydiv]
q:57 [binder, in mathcomp.field.fieldext]
Q:57 [binder, in mathcomp.ssreflect.ssrbool]
q:572 [binder, in mathcomp.algebra.polydiv]
q:582 [binder, in mathcomp.algebra.polydiv]
q:584 [binder, in mathcomp.algebra.polydiv]
q:586 [binder, in mathcomp.algebra.polydiv]
q:587 [binder, in mathcomp.algebra.poly]
q:589 [binder, in mathcomp.algebra.poly]
q:59 [binder, in mathcomp.algebra.polydiv]
q:59 [binder, in mathcomp.field.separable]
Q:59 [binder, in mathcomp.solvable.sylow]
q:59 [binder, in mathcomp.algebra.poly]
q:593 [binder, in mathcomp.algebra.poly]
q:595 [binder, in mathcomp.algebra.polydiv]
q:595 [binder, in mathcomp.algebra.poly]
q:597 [binder, in mathcomp.algebra.polydiv]
Q:6 [binder, in mathcomp.solvable.primitive_action]
Q:6 [binder, in mathcomp.algebra.ring_quotient]
q:60 [binder, in mathcomp.field.fieldext]
q:60 [binder, in mathcomp.field.qfpoly]
q:60 [binder, in mathcomp.algebra.polyXY]
q:601 [binder, in mathcomp.algebra.mxalgebra]
q:603 [binder, in mathcomp.algebra.polydiv]
q:606 [binder, in mathcomp.algebra.polydiv]
q:608 [binder, in mathcomp.algebra.polydiv]
q:608 [binder, in mathcomp.algebra.poly]
q:608 [binder, in mathcomp.algebra.mxalgebra]
q:61 [binder, in mathcomp.algebra.polydiv]
q:612 [binder, in mathcomp.algebra.polydiv]
q:615 [binder, in mathcomp.algebra.polydiv]
q:616 [binder, in mathcomp.algebra.polydiv]
q:618 [binder, in mathcomp.algebra.polydiv]
q:621 [binder, in mathcomp.algebra.polydiv]
q:622 [binder, in mathcomp.algebra.mxalgebra]
q:624 [binder, in mathcomp.algebra.polydiv]
q:627 [binder, in mathcomp.algebra.polydiv]
q:629 [binder, in mathcomp.algebra.poly]
q:629 [binder, in mathcomp.algebra.mxalgebra]
q:63 [binder, in mathcomp.algebra.polydiv]
Q:63 [binder, in mathcomp.solvable.sylow]
q:631 [binder, in mathcomp.algebra.poly]
q:632 [binder, in mathcomp.algebra.polydiv]
q:634 [binder, in mathcomp.algebra.poly]
q:636 [binder, in mathcomp.algebra.poly]
q:637 [binder, in mathcomp.algebra.polydiv]
q:64 [binder, in mathcomp.field.closed_field]
q:640 [binder, in mathcomp.algebra.polydiv]
q:643 [binder, in mathcomp.algebra.polydiv]
q:646 [binder, in mathcomp.algebra.polydiv]
q:649 [binder, in mathcomp.algebra.polydiv]
q:652 [binder, in mathcomp.algebra.polydiv]
q:655 [binder, in mathcomp.algebra.polydiv]
q:658 [binder, in mathcomp.algebra.polydiv]
q:663 [binder, in mathcomp.ssreflect.order]
q:665 [binder, in mathcomp.ssreflect.order]
q:669 [binder, in mathcomp.ssreflect.order]
q:67 [binder, in mathcomp.algebra.polyXY]
q:670 [binder, in mathcomp.algebra.polydiv]
q:671 [binder, in mathcomp.ssreflect.order]
q:673 [binder, in mathcomp.algebra.polydiv]
q:676 [binder, in mathcomp.algebra.poly]
q:678 [binder, in mathcomp.algebra.poly]
q:681 [binder, in mathcomp.algebra.poly]
q:683 [binder, in mathcomp.algebra.poly]
q:69 [binder, in mathcomp.algebra.mxpoly]
q:691 [binder, in mathcomp.algebra.polydiv]
q:693 [binder, in mathcomp.algebra.polydiv]
q:697 [binder, in mathcomp.algebra.polydiv]
Q:7 [binder, in mathcomp.solvable.primitive_action]
q:7 [binder, in mathcomp.ssreflect.prime]
q:7 [binder, in mathcomp.solvable.extremal]
Q:70 [binder, in mathcomp.ssreflect.choice]
Q:70 [binder, in mathcomp.algebra.ring_quotient]
q:700 [binder, in mathcomp.algebra.polydiv]
q:703 [binder, in mathcomp.algebra.polydiv]
q:706 [binder, in mathcomp.algebra.polydiv]
q:709 [binder, in mathcomp.algebra.polydiv]
q:71 [binder, in mathcomp.field.qfpoly]
q:71 [binder, in mathcomp.algebra.polyXY]
q:711 [binder, in mathcomp.algebra.polydiv]
q:718 [binder, in mathcomp.algebra.polydiv]
q:72 [binder, in mathcomp.algebra.polydiv]
q:726 [binder, in mathcomp.algebra.polydiv]
q:73 [binder, in mathcomp.field.qfpoly]
q:73 [binder, in mathcomp.algebra.polyXY]
q:731 [binder, in mathcomp.algebra.polydiv]
q:733 [binder, in mathcomp.algebra.polydiv]
q:739 [binder, in mathcomp.algebra.polydiv]
q:74 [binder, in mathcomp.field.separable]
q:740 [binder, in mathcomp.algebra.polydiv]
q:743 [binder, in mathcomp.algebra.polydiv]
q:746 [binder, in mathcomp.algebra.polydiv]
q:748 [binder, in mathcomp.algebra.polydiv]
q:75 [binder, in mathcomp.field.qfpoly]
q:751 [binder, in mathcomp.algebra.polydiv]
q:753 [binder, in mathcomp.algebra.polydiv]
q:757 [binder, in mathcomp.algebra.polydiv]
q:760 [binder, in mathcomp.algebra.polydiv]
q:763 [binder, in mathcomp.algebra.polydiv]
q:765 [binder, in mathcomp.algebra.polydiv]
q:768 [binder, in mathcomp.algebra.polydiv]
q:780 [binder, in mathcomp.algebra.polydiv]
q:782 [binder, in mathcomp.algebra.polydiv]
q:787 [binder, in mathcomp.algebra.poly]
q:79 [binder, in mathcomp.algebra.fraction]
q:794 [binder, in mathcomp.algebra.poly]
q:799 [binder, in mathcomp.algebra.poly]
Q:8 [binder, in mathcomp.solvable.primitive_action]
q:80 [binder, in mathcomp.field.qfpoly]
q:80 [binder, in mathcomp.ssreflect.prime]
q:80 [binder, in mathcomp.algebra.polyXY]
q:801 [binder, in mathcomp.ssreflect.path]
q:802 [binder, in mathcomp.ssreflect.path]
q:806 [binder, in mathcomp.algebra.poly]
q:81 [binder, in mathcomp.field.algebraics_fundamentals]
q:81 [binder, in mathcomp.algebra.poly]
q:816 [binder, in mathcomp.algebra.poly]
q:819 [binder, in mathcomp.algebra.poly]
q:82 [binder, in mathcomp.algebra.polydiv]
q:820 [binder, in mathcomp.algebra.polydiv]
q:823 [binder, in mathcomp.algebra.polydiv]
q:823 [binder, in mathcomp.algebra.poly]
q:826 [binder, in mathcomp.algebra.polydiv]
q:828 [binder, in mathcomp.algebra.poly]
q:829 [binder, in mathcomp.algebra.polydiv]
q:83 [binder, in mathcomp.algebra.mxpoly]
q:832 [binder, in mathcomp.algebra.poly]
q:834 [binder, in mathcomp.algebra.polydiv]
q:840 [binder, in mathcomp.algebra.polydiv]
q:842 [binder, in mathcomp.algebra.polydiv]
q:845 [binder, in mathcomp.algebra.poly]
q:846 [binder, in mathcomp.algebra.polydiv]
q:848 [binder, in mathcomp.algebra.polydiv]
q:849 [binder, in mathcomp.algebra.polydiv]
Q:85 [binder, in mathcomp.ssreflect.choice]
q:850 [binder, in mathcomp.algebra.polydiv]
q:851 [binder, in mathcomp.algebra.polydiv]
q:853 [binder, in mathcomp.algebra.polydiv]
q:855 [binder, in mathcomp.algebra.polydiv]
q:857 [binder, in mathcomp.algebra.poly]
q:86 [binder, in mathcomp.ssreflect.prime]
q:860 [binder, in mathcomp.algebra.polydiv]
q:864 [binder, in mathcomp.algebra.polydiv]
q:866 [binder, in mathcomp.algebra.polydiv]
q:868 [binder, in mathcomp.algebra.polydiv]
q:87 [binder, in mathcomp.algebra.mxpoly]
q:871 [binder, in mathcomp.algebra.poly]
q:872 [binder, in mathcomp.algebra.polydiv]
q:874 [binder, in mathcomp.algebra.polydiv]
q:88 [binder, in mathcomp.algebra.polydiv]
q:88 [binder, in mathcomp.solvable.finmodule]
q:88 [binder, in mathcomp.algebra.poly]
q:881 [binder, in mathcomp.algebra.polydiv]
q:883 [binder, in mathcomp.algebra.polydiv]
q:886 [binder, in mathcomp.algebra.polydiv]
q:888 [binder, in mathcomp.algebra.polydiv]
q:89 [binder, in mathcomp.ssreflect.prime]
q:89 [binder, in mathcomp.algebra.polyXY]
q:895 [binder, in mathcomp.algebra.polydiv]
q:897 [binder, in mathcomp.algebra.polydiv]
q:898 [binder, in mathcomp.algebra.poly]
Q:9 [binder, in mathcomp.solvable.primitive_action]
q:90 [binder, in mathcomp.field.closed_field]
q:90 [binder, in mathcomp.algebra.poly]
q:901 [binder, in mathcomp.algebra.polydiv]
q:905 [binder, in mathcomp.algebra.polydiv]
q:909 [binder, in mathcomp.algebra.polydiv]
q:910 [binder, in mathcomp.algebra.polydiv]
q:913 [binder, in mathcomp.algebra.polydiv]
q:915 [binder, in mathcomp.algebra.mxalgebra]
q:918 [binder, in mathcomp.algebra.polydiv]
Q:92 [binder, in mathcomp.ssreflect.choice]
q:920 [binder, in mathcomp.algebra.polydiv]
q:922 [binder, in mathcomp.algebra.polydiv]
q:924 [binder, in mathcomp.algebra.poly]
q:925 [binder, in mathcomp.algebra.polydiv]
q:93 [binder, in mathcomp.algebra.polyXY]
q:932 [binder, in mathcomp.ssreflect.ssrnat]
q:934 [binder, in mathcomp.algebra.polydiv]
q:936 [binder, in mathcomp.ssreflect.ssrnat]
q:937 [binder, in mathcomp.algebra.polydiv]
q:94 [binder, in mathcomp.algebra.polydiv]
Q:94 [binder, in mathcomp.algebra.ring_quotient]
q:940 [binder, in mathcomp.algebra.polydiv]
q:940 [binder, in mathcomp.ssreflect.ssrnat]
q:942 [binder, in mathcomp.algebra.poly]
q:944 [binder, in mathcomp.ssreflect.ssrnat]
q:95 [binder, in mathcomp.algebra.polydiv]
q:95 [binder, in mathcomp.field.closed_field]
q:953 [binder, in mathcomp.algebra.polydiv]
q:956 [binder, in mathcomp.algebra.polydiv]
q:958 [binder, in mathcomp.algebra.polydiv]
q:962 [binder, in mathcomp.algebra.polydiv]
q:964 [binder, in mathcomp.algebra.polydiv]
q:966 [binder, in mathcomp.algebra.polydiv]
q:968 [binder, in mathcomp.algebra.poly]
q:969 [binder, in mathcomp.algebra.polydiv]
q:97 [binder, in mathcomp.algebra.polyXY]
q:971 [binder, in mathcomp.algebra.polydiv]
q:973 [binder, in mathcomp.algebra.polydiv]
q:973 [binder, in mathcomp.algebra.poly]
q:976 [binder, in mathcomp.algebra.polydiv]
q:976 [binder, in mathcomp.algebra.poly]
q:979 [binder, in mathcomp.algebra.polydiv]
q:98 [binder, in mathcomp.field.closed_field]
Q:980 [binder, in mathcomp.ssreflect.fintype]
q:990 [binder, in mathcomp.algebra.polydiv]
q:993 [binder, in mathcomp.algebra.polydiv]
q:996 [binder, in mathcomp.algebra.polydiv]

---

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

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

(1892 entries)

Binder 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

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

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

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

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

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

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

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

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

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

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

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

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

(36 entries)

---

Index

---

This page has been generated by coqdoc