mathcomp.ssreflect.tuple

Global Index

_

(75489 entries)

Notation Index

H

J

T

W

X

Y

_

(1813 entries)

Binder Index

_

other

(45320 entries)

Module Index

H

J

K

L

W

X

Y

Z

_

other

(382 entries)

Variable Index

J

W

X

Y

_

other

(3967 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(14046 entries)

Constructor Index

J

K

W

Y

_

other

(469 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(128 entries)

Projection Index

H

J

K

L

W

X

Y

_

other

(457 entries)

Section Index

J

W

X

Y

_

other

(1372 entries)

Abbreviation Index

Y

_

other

(1025 entries)

Definition Index

Y

_

other

(6124 entries)

Record Index

H

J

K

L

W

X

Y

_

other

(250 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]
qc:107 [binder, in mathcomp.algebra.ring_quotient]
qc:110 [binder, in mathcomp.ssreflect.generic_quotient]
qc:112 [binder, in mathcomp.algebra.ring_quotient]
qc:130 [binder, in mathcomp.ssreflect.generic_quotient]
qc:144 [binder, in mathcomp.algebra.ring_quotient]
qc:179 [binder, in mathcomp.algebra.ring_quotient]
qc:184 [binder, in mathcomp.algebra.ring_quotient]
qc:36 [binder, in mathcomp.algebra.ring_quotient]
qc:41 [binder, in mathcomp.algebra.ring_quotient]
qc:7 [binder, in mathcomp.algebra.ring_quotient]
qc:76 [binder, in mathcomp.algebra.ring_quotient]
QEdecFieldMixin [abbreviation, in mathcomp.algebra.ssralg]
QeqT:2414 [binder, in mathcomp.algebra.ssralg]
qev:1970 [binder, in mathcomp.algebra.ssralg]
qev:2000 [binder, in mathcomp.algebra.ssralg]
qf_eval [abbreviation, in mathcomp.character.mxrepresentation]
qf_form [abbreviation, in mathcomp.character.mxrepresentation]
qf:2285 [binder, in mathcomp.algebra.ssralg]
qf:2288 [binder, in mathcomp.algebra.ssralg]
Qint [definition, in mathcomp.algebra.rat]
QintP [lemma, in mathcomp.algebra.rat]
QintPred [section, in mathcomp.algebra.rat]
Qint_dvdz [lemma, in mathcomp.algebra.intdiv]
Qint_subringPred [definition, in mathcomp.algebra.rat]
Qint_smulrPred [definition, in mathcomp.algebra.rat]
Qint_semiringPred [definition, in mathcomp.algebra.rat]
Qint_zmodPred [definition, in mathcomp.algebra.rat]
Qint_mulrPred [definition, in mathcomp.algebra.rat]
Qint_addrPred [definition, in mathcomp.algebra.rat]
Qint_opprPred [definition, in mathcomp.algebra.rat]
Qint_subring_closed [lemma, in mathcomp.algebra.rat]
Qint_def [lemma, in mathcomp.algebra.rat]
Qint_keyed [definition, in mathcomp.algebra.rat]
Qint_key [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]
Qmorphism [abbreviation, in mathcomp.field.algebraics_fundamentals]
Qnat [definition, in mathcomp.algebra.rat]
QnatP [lemma, in mathcomp.algebra.rat]
QnatPred [section, in mathcomp.algebra.rat]
Qnat_dvd [lemma, in mathcomp.algebra.intdiv]
Qnat_semiringPred [definition, in mathcomp.algebra.rat]
Qnat_mulrPred [definition, in mathcomp.algebra.rat]
Qnat_addrPred [definition, in mathcomp.algebra.rat]
Qnat_semiring_closed [lemma, in mathcomp.algebra.rat]
Qnat_def [lemma, in mathcomp.algebra.rat]
Qnat_keyed [definition, in mathcomp.algebra.rat]
Qnat_key [lemma, in mathcomp.algebra.rat]
QnC:10 [binder, in mathcomp.character.integral_char]
QnC:115 [binder, in mathcomp.field.algnum]
QnC:5 [binder, in mathcomp.character.integral_char]
Qn_aut_exists [lemma, in mathcomp.field.algnum]
Qn:114 [binder, in mathcomp.field.algnum]
Qn:3 [binder, in mathcomp.character.integral_char]
Qn:4 [binder, in mathcomp.character.integral_char]
qq1:11 [binder, in mathcomp.algebra.polydiv]
qq1:130 [binder, in mathcomp.field.closed_field]
qq1:142 [binder, in mathcomp.field.closed_field]
qq:1014 [binder, in mathcomp.algebra.polydiv]
qq:123 [binder, in mathcomp.field.closed_field]
qq:137 [binder, in mathcomp.field.closed_field]
qq:147 [binder, in mathcomp.field.closed_field]
qq:154 [binder, in mathcomp.field.closed_field]
qq:157 [binder, in mathcomp.algebra.polydiv]
qq:163 [binder, in mathcomp.field.closed_field]
qq:175 [binder, in mathcomp.field.closed_field]
qq:180 [binder, in mathcomp.field.closed_field]
qq:204 [binder, in mathcomp.field.closed_field]
qq:210 [binder, in mathcomp.field.closed_field]
qq:465 [binder, in mathcomp.algebra.polydiv]
qq:474 [binder, in mathcomp.algebra.polydiv]
qq:6 [binder, in mathcomp.algebra.polydiv]
qq:67 [binder, in mathcomp.algebra.polydiv]
qq:76 [binder, in mathcomp.algebra.polydiv]
qq:781 [binder, in mathcomp.algebra.polydiv]
QrC:209 [binder, in mathcomp.field.algnum]
QrC:213 [binder, in mathcomp.field.algnum]
Qr:201 [binder, in mathcomp.field.algnum]
Qr:202 [binder, in mathcomp.field.algnum]
QsC:196 [binder, in mathcomp.field.algnum]
QsC:27 [binder, in mathcomp.field.algnum]
QsC:31 [binder, in mathcomp.field.algnum]
Qs:195 [binder, in mathcomp.field.algnum]
Qs:2241 [binder, in mathcomp.ssreflect.seq]
Qs:26 [binder, in mathcomp.field.algnum]
Qs:30 [binder, in mathcomp.field.algnum]
qs:372 [binder, in mathcomp.ssreflect.div]
qs:378 [binder, in mathcomp.ssreflect.div]
QtoC [abbreviation, in mathcomp.field.cyclotomic]
QtoC [abbreviation, in mathcomp.field.algC]
QtoC [abbreviation, in mathcomp.field.algnum]
QtoCm [abbreviation, in mathcomp.field.algC]
QtoCm [abbreviation, in mathcomp.field.algnum]
QtoCm:130 [binder, in mathcomp.field.algC]
QtoC_M [abbreviation, in mathcomp.field.cyclotomic]
QtoC:16 [binder, in mathcomp.field.algebraics_fundamentals]
QtoC:2 [binder, in mathcomp.field.algebraics_fundamentals]
qT:105 [binder, in mathcomp.algebra.ring_quotient]
qT:11 [binder, in mathcomp.ssreflect.generic_quotient]
qT:111 [binder, in mathcomp.algebra.ring_quotient]
qT:119 [binder, in mathcomp.algebra.ring_quotient]
qT:128 [binder, in mathcomp.ssreflect.generic_quotient]
qT:14 [binder, in mathcomp.ssreflect.generic_quotient]
qT:156 [binder, in mathcomp.ssreflect.generic_quotient]
qT:158 [binder, in mathcomp.ssreflect.generic_quotient]
qT:160 [binder, in mathcomp.ssreflect.generic_quotient]
qT:162 [binder, in mathcomp.ssreflect.generic_quotient]
qT:177 [binder, in mathcomp.algebra.ring_quotient]
qT:18 [binder, in mathcomp.ssreflect.generic_quotient]
qT:183 [binder, in mathcomp.algebra.ring_quotient]
qT:191 [binder, in mathcomp.algebra.ring_quotient]
qT:2 [binder, in mathcomp.ssreflect.generic_quotient]
qT:34 [binder, in mathcomp.algebra.ring_quotient]
qT:40 [binder, in mathcomp.algebra.ring_quotient]
qT:42 [binder, in mathcomp.ssreflect.generic_quotient]
qT:49 [binder, in mathcomp.algebra.ring_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_gtype [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]
QuotClass [constructor, in mathcomp.ssreflect.generic_quotient]
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.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.kI [variable, in mathcomp.algebra.ring_quotient]
Quotient.IDomainQuotient.pidealI [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.RingQuotient [section, in mathcomp.algebra.ring_quotient]
Quotient.RingQuotient.I [variable, in mathcomp.algebra.ring_quotient]
Quotient.RingQuotient.idealI [variable, in mathcomp.algebra.ring_quotient]
Quotient.RingQuotient.kI [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.rquot_ringQuotType [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_ringQuotMixin [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_comRingType [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_ringType [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_comRingMixin [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_zmodQuotType [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_zmodQuotMixin [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_zmodType [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_zmodMixin [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_eqQuotType [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_choiceType [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_eqType [definition, in mathcomp.algebra.ring_quotient]
Quotient.rquot_quotType [definition, in mathcomp.algebra.ring_quotient]
Quotient.type [abbreviation, in mathcomp.algebra.ring_quotient]
Quotient.type [definition, in mathcomp.algebra.ring_quotient]
Quotient.type_of [definition, 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.kI [variable, in mathcomp.algebra.ring_quotient]
Quotient.ZmodQuotient.R [variable, in mathcomp.algebra.ring_quotient]
Quotient.ZmodQuotient.zmodI [variable, in mathcomp.algebra.ring_quotient]
{quot _ } [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.choiceMixin [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.choiceType [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.countMixin [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.countType [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.eqMixin [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.eqType [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.finMixin [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.finType [section, in mathcomp.ssreflect.generic_quotient]
QuotSubType.finType.qT [variable, in mathcomp.ssreflect.generic_quotient]
QuotSubType.finType.T [variable, in mathcomp.ssreflect.generic_quotient]
QuotSubType.qreprK [lemma, 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]
QuotSubType.subCountType [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.subType [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.SubTypeMixin [section, in mathcomp.ssreflect.generic_quotient]
QuotSubType.SubTypeMixin.qT [variable, in mathcomp.ssreflect.generic_quotient]
QuotSubType.SubTypeMixin.T [variable, in mathcomp.ssreflect.generic_quotient]
QuotType [abbreviation, in mathcomp.ssreflect.generic_quotient]
quotType [record, in mathcomp.ssreflect.generic_quotient]
QuotTypePack [constructor, 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]
QuotType_clone [definition, in mathcomp.ssreflect.generic_quotient]
quotW [lemma, in mathcomp.ssreflect.generic_quotient]
quot_class_of [abbreviation, in mathcomp.ssreflect.generic_quotient]
quot_class [projection, in mathcomp.ssreflect.generic_quotient]
quot_sort [projection, in mathcomp.ssreflect.generic_quotient]
quot_class_of [abbreviation, in mathcomp.ssreflect.generic_quotient]
quot_pi [projection, in mathcomp.ssreflect.generic_quotient]
quot_repr [projection, in mathcomp.ssreflect.generic_quotient]
quot_mixin_of [record, 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:307 [binder, in mathcomp.algebra.polydiv]
Qxz:126 [binder, in mathcomp.field.algebraics_fundamentals]
Qxz:130 [binder, in mathcomp.field.algebraics_fundamentals]
Qz1:74 [binder, in mathcomp.field.algnum]
Qz1:77 [binder, in mathcomp.field.algnum]
Qz2:75 [binder, in mathcomp.field.algnum]
Qz2:78 [binder, in mathcomp.field.algnum]
Qz:67 [binder, in mathcomp.field.algnum]
Qz:69 [binder, in mathcomp.field.algebraics_fundamentals]
Qz:69 [binder, in mathcomp.field.algnum]
q_k:71 [binder, in mathcomp.field.algC]
q_:3338 [binder, in mathcomp.algebra.matrix]
q_:3323 [binder, in mathcomp.algebra.matrix]
q_:3123 [binder, in mathcomp.algebra.matrix]
q_:3065 [binder, in mathcomp.algebra.matrix]
q_:2981 [binder, in mathcomp.algebra.matrix]
q_:2874 [binder, in mathcomp.algebra.matrix]
q_:2805 [binder, in mathcomp.algebra.matrix]
q_:2777 [binder, in mathcomp.algebra.matrix]
q_:2766 [binder, in mathcomp.algebra.matrix]
q_:2754 [binder, in mathcomp.algebra.matrix]
q_:2742 [binder, in mathcomp.algebra.matrix]
q_:2680 [binder, in mathcomp.algebra.matrix]
q_:2495 [binder, in mathcomp.algebra.matrix]
q_unitP:391 [binder, in mathcomp.field.closed_field]
q1:114 [binder, in mathcomp.algebra.polydiv]
q1:121 [binder, in mathcomp.algebra.polydiv]
q1:153 [binder, in mathcomp.algebra.polydiv]
q1:228 [binder, in mathcomp.field.closed_field]
q1:232 [binder, in mathcomp.field.closed_field]
q1:260 [binder, in mathcomp.field.algnum]
q1:269 [binder, in mathcomp.field.algnum]
q1:542 [binder, in mathcomp.algebra.polydiv]
q1:912 [binder, in mathcomp.algebra.polydiv]
q1:919 [binder, in mathcomp.algebra.polydiv]
q2:246 [binder, in mathcomp.field.galois]
q2:543 [binder, in mathcomp.algebra.polydiv]
q2:913 [binder, in mathcomp.algebra.polydiv]
q2:920 [binder, in mathcomp.algebra.polydiv]
Q8_extraspecial [lemma, in mathcomp.solvable.extraspecial]
q:1 [binder, in mathcomp.ssreflect.prime]
Q:10 [binder, in mathcomp.ssreflect.generic_quotient]
q:10 [binder, in mathcomp.algebra.polyXY]
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.algebra.polydiv]
q:1010 [binder, in mathcomp.algebra.polydiv]
q:1013 [binder, in mathcomp.algebra.polydiv]
q:1016 [binder, in mathcomp.algebra.polydiv]
q:1019 [binder, in mathcomp.algebra.polydiv]
q:1022 [binder, in mathcomp.algebra.polydiv]
q:1023 [binder, in mathcomp.algebra.poly]
q:103 [binder, in mathcomp.algebra.polydiv]
Q:103 [binder, in mathcomp.ssreflect.choice]
q:1035 [binder, in mathcomp.algebra.polydiv]
q:1037 [binder, in mathcomp.algebra.polydiv]
q:1039 [binder, in mathcomp.algebra.polydiv]
Q:104 [binder, in mathcomp.algebra.ring_quotient]
q:1041 [binder, in mathcomp.algebra.polydiv]
Q:1042 [binder, in mathcomp.ssreflect.bigop]
q:1043 [binder, in mathcomp.algebra.polydiv]
q:1045 [binder, in mathcomp.algebra.polydiv]
q:1047 [binder, in mathcomp.algebra.polydiv]
q:1049 [binder, in mathcomp.algebra.polydiv]
q:105 [binder, in mathcomp.field.closed_field]
q:1051 [binder, in mathcomp.algebra.polydiv]
Q:1053 [binder, in mathcomp.ssreflect.bigop]
q:1054 [binder, in mathcomp.algebra.polydiv]
q:1057 [binder, in mathcomp.algebra.polydiv]
q:106 [binder, in mathcomp.field.algC]
q:1060 [binder, in mathcomp.algebra.polydiv]
q:1079 [binder, in mathcomp.algebra.poly]
q:108 [binder, in mathcomp.algebra.polydiv]
q:1087 [binder, in mathcomp.algebra.poly]
Q:109 [binder, in mathcomp.ssreflect.generic_quotient]
q:11 [binder, in mathcomp.ssreflect.div]
Q:110 [binder, in mathcomp.ssreflect.choice]
Q:110 [binder, in mathcomp.algebra.ring_quotient]
q:110 [binder, in mathcomp.field.finfield]
q:1102 [binder, in mathcomp.ssreflect.ssrnat]
q:1104 [binder, in mathcomp.ssreflect.ssrnat]
q:112 [binder, in mathcomp.field.closed_field]
q:112 [binder, in mathcomp.character.mxabelem]
q:115 [binder, in mathcomp.character.mxabelem]
Q:116 [binder, in mathcomp.ssreflect.generic_quotient]
q:1162 [binder, in mathcomp.algebra.mxalgebra]
q:117 [binder, in mathcomp.algebra.polydiv]
Q:118 [binder, in mathcomp.algebra.ring_quotient]
q:119 [binder, in mathcomp.field.closed_field]
q:119 [binder, in mathcomp.character.mxabelem]
Q:119 [binder, in mathcomp.solvable.gseries]
q:12 [binder, in mathcomp.algebra.polyXY]
Q:121 [binder, in mathcomp.solvable.gseries]
q:122 [binder, in mathcomp.character.mxabelem]
Q:1255 [binder, in mathcomp.ssreflect.finset]
Q:1257 [binder, in mathcomp.ssreflect.finset]
Q:1259 [binder, in mathcomp.ssreflect.finset]
Q:127 [binder, in mathcomp.ssreflect.generic_quotient]
q:1284 [binder, in mathcomp.algebra.matrix]
q:129 [binder, in mathcomp.ssreflect.prime]
q:1291 [binder, in mathcomp.algebra.matrix]
q:130 [binder, in mathcomp.algebra.polydiv]
q:130 [binder, in mathcomp.algebra.poly]
q:132 [binder, in mathcomp.algebra.poly]
Q:133 [binder, in mathcomp.ssreflect.generic_quotient]
q:133 [binder, in mathcomp.field.closed_field]
q:134 [binder, in mathcomp.algebra.polydiv]
q:136 [binder, in mathcomp.algebra.polydiv]
q:139 [binder, in mathcomp.algebra.polydiv]
Q:140 [binder, in mathcomp.ssreflect.choice]
q:142 [binder, in mathcomp.field.algC]
q:143 [binder, in mathcomp.algebra.polydiv]
Q:143 [binder, in mathcomp.algebra.ring_quotient]
Q:1438 [binder, in mathcomp.ssreflect.bigop]
q:144 [binder, in mathcomp.algebra.poly]
q:146 [binder, in mathcomp.algebra.poly]
q:147 [binder, in mathcomp.algebra.polydiv]
Q:147 [binder, in mathcomp.solvable.hall]
Q:1474 [binder, in mathcomp.ssreflect.finset]
q:1478 [binder, in mathcomp.algebra.matrix]
q:148 [binder, in mathcomp.algebra.poly]
q:15 [binder, in mathcomp.algebra.polydiv]
q:150 [binder, in mathcomp.algebra.polydiv]
q:150 [binder, in mathcomp.field.closed_field]
q:152 [binder, in mathcomp.algebra.polydiv]
Q:152 [binder, in mathcomp.algebra.ring_quotient]
q:154 [binder, in mathcomp.algebra.poly]
q:159 [binder, in mathcomp.field.closed_field]
q:160 [binder, in mathcomp.algebra.poly]
q:164 [binder, in mathcomp.field.falgebra]
Q:1647 [binder, in mathcomp.ssreflect.bigop]
Q:1665 [binder, in mathcomp.ssreflect.bigop]
q:167 [binder, in mathcomp.algebra.intdiv]
q:168 [binder, in mathcomp.field.closed_field]
Q:1683 [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.ring_quotient]
q:17 [binder, in mathcomp.algebra.polyXY]
Q:170 [binder, in mathcomp.solvable.sylow]
Q:1711 [binder, in mathcomp.ssreflect.bigop]
q:173 [binder, in mathcomp.algebra.polydiv]
q:173 [binder, in mathcomp.field.algebraics_fundamentals]
q:173 [binder, in mathcomp.field.closed_field]
Q:1734 [binder, in mathcomp.ssreflect.bigop]
Q:1753 [binder, in mathcomp.ssreflect.bigop]
Q:176 [binder, in mathcomp.algebra.ring_quotient]
q:1762 [binder, in mathcomp.algebra.matrix]
Q:1776 [binder, in mathcomp.ssreflect.bigop]
q:178 [binder, in mathcomp.algebra.mxpoly]
q:18 [binder, in mathcomp.algebra.polyXY]
q:18 [binder, in mathcomp.solvable.extremal]
q:180 [binder, in mathcomp.algebra.mxpoly]
q:181 [binder, in mathcomp.algebra.polydiv]
Q:182 [binder, in mathcomp.algebra.ring_quotient]
q:182 [binder, in mathcomp.algebra.mxpoly]
q:183 [binder, in mathcomp.field.algebraics_fundamentals]
q:184 [binder, in mathcomp.field.algebraics_fundamentals]
q:184 [binder, in mathcomp.field.closed_field]
Q:1841 [binder, in mathcomp.ssreflect.bigop]
q:187 [binder, in mathcomp.algebra.poly]
q:1877 [binder, in mathcomp.algebra.ssrnum]
q:188 [binder, in mathcomp.field.closed_field]
Q:1883 [binder, in mathcomp.ssreflect.bigop]
q:19 [binder, in mathcomp.algebra.polydiv]
q:19 [binder, in mathcomp.algebra.polyXY]
q:19 [binder, in mathcomp.algebra.poly]
Q:190 [binder, in mathcomp.algebra.ring_quotient]
Q:1901 [binder, in mathcomp.ssreflect.bigop]
q:191 [binder, in mathcomp.algebra.polydiv]
q:191 [binder, in mathcomp.field.closed_field]
q:192 [binder, in mathcomp.field.algebraics_fundamentals]
Q:1920 [binder, in mathcomp.ssreflect.bigop]
q:193 [binder, in mathcomp.algebra.polydiv]
q:193 [binder, in mathcomp.algebra.poly]
q:194 [binder, in mathcomp.field.algebraics_fundamentals]
q:194 [binder, in mathcomp.field.closed_field]
Q:194 [binder, in mathcomp.ssreflect.fintype]
q:195 [binder, in mathcomp.algebra.polydiv]
q:197 [binder, in mathcomp.algebra.polydiv]
q:197 [binder, in mathcomp.field.closed_field]
q:198 [binder, in mathcomp.field.algebraics_fundamentals]
q:199 [binder, in mathcomp.algebra.polydiv]
q:199 [binder, in mathcomp.algebra.poly]
q:2 [binder, in mathcomp.algebra.polydiv]
q:20 [binder, in mathcomp.algebra.polyXY]
q:200 [binder, in mathcomp.field.closed_field]
Q:2002 [binder, in mathcomp.ssreflect.seq]
q:201 [binder, in mathcomp.algebra.polydiv]
q:201 [binder, in mathcomp.algebra.poly]
Q:2020 [binder, in mathcomp.ssreflect.seq]
q:203 [binder, in mathcomp.algebra.poly]
q:204 [binder, in mathcomp.algebra.polydiv]
q:205 [binder, in mathcomp.algebra.poly]
q:206 [binder, in mathcomp.algebra.polydiv]
q:208 [binder, in mathcomp.algebra.polydiv]
q:21 [binder, in mathcomp.algebra.polydiv]
q:21 [binder, in mathcomp.field.separable]
q:21 [binder, in mathcomp.algebra.polyXY]
q:210 [binder, in mathcomp.algebra.polydiv]
Q:211 [binder, in mathcomp.ssreflect.ssrbool]
q:212 [binder, in mathcomp.algebra.polydiv]
Q:213 [binder, in mathcomp.ssreflect.ssrbool]
q:214 [binder, in mathcomp.algebra.polydiv]
q:216 [binder, in mathcomp.algebra.polydiv]
q:216 [binder, in mathcomp.ssreflect.prime]
q:218 [binder, in mathcomp.ssreflect.fingraph]
q:220 [binder, in mathcomp.field.closed_field]
q:220 [binder, in mathcomp.ssreflect.fingraph]
q:222 [binder, in mathcomp.algebra.polydiv]
q:222 [binder, in mathcomp.ssreflect.fingraph]
Q:2235 [binder, in mathcomp.ssreflect.seq]
q:224 [binder, in mathcomp.algebra.polydiv]
q:224 [binder, in mathcomp.field.closed_field]
q:226 [binder, in mathcomp.field.closed_field]
q:229 [binder, in mathcomp.algebra.polydiv]
q:23 [binder, in mathcomp.algebra.polydiv]
q:23 [binder, in mathcomp.field.separable]
q:23 [binder, in mathcomp.algebra.mxpoly]
q:232 [binder, in mathcomp.algebra.polydiv]
q:233 [binder, in mathcomp.algebra.polydiv]
q:235 [binder, in mathcomp.field.galois]
q:236 [binder, in mathcomp.ssreflect.seq]
q:239 [binder, in mathcomp.algebra.polydiv]
q:239 [binder, in mathcomp.field.closed_field]
Q:2412 [binder, in mathcomp.algebra.ssralg]
q:242 [binder, in mathcomp.field.closed_field]
q:243 [binder, in mathcomp.algebra.poly]
q:244 [binder, in mathcomp.algebra.polydiv]
q:245 [binder, in mathcomp.algebra.poly]
q:246 [binder, in mathcomp.algebra.polydiv]
q:2479 [binder, in mathcomp.algebra.matrix]
q:2493 [binder, in mathcomp.algebra.matrix]
q:25 [binder, in mathcomp.algebra.polydiv]
q:25 [binder, in mathcomp.field.separable]
q:251 [binder, in mathcomp.algebra.polydiv]
q:253 [binder, in mathcomp.algebra.polydiv]
q:253 [binder, in mathcomp.algebra.poly]
q:257 [binder, in mathcomp.algebra.mxpoly]
q:257 [binder, in mathcomp.field.closed_field]
q:26 [binder, in mathcomp.ssreflect.path]
q:261 [binder, in mathcomp.algebra.polydiv]
q:262 [binder, in mathcomp.algebra.intdiv]
q:265 [binder, in mathcomp.algebra.polydiv]
q:2678 [binder, in mathcomp.algebra.matrix]
q:269 [binder, in mathcomp.field.closed_field]
q:271 [binder, in mathcomp.algebra.polydiv]
q:272 [binder, in mathcomp.solvable.extremal]
q:273 [binder, in mathcomp.algebra.polydiv]
q:274 [binder, in mathcomp.field.closed_field]
q:2740 [binder, in mathcomp.algebra.matrix]
q:275 [binder, in mathcomp.field.closed_field]
q:2752 [binder, in mathcomp.algebra.matrix]
q:2764 [binder, in mathcomp.algebra.matrix]
q:277 [binder, in mathcomp.algebra.polydiv]
q:2776 [binder, in mathcomp.algebra.matrix]
q:2804 [binder, in mathcomp.algebra.matrix]
q:281 [binder, in mathcomp.algebra.polydiv]
q:282 [binder, in mathcomp.field.closed_field]
q:283 [binder, in mathcomp.algebra.polydiv]
q:285 [binder, in mathcomp.algebra.polydiv]
q:285 [binder, in mathcomp.field.closed_field]
q:287 [binder, in mathcomp.field.closed_field]
q:29 [binder, in mathcomp.algebra.polydiv]
q:292 [binder, in mathcomp.algebra.polydiv]
q:292 [binder, in mathcomp.field.closed_field]
q:296 [binder, in mathcomp.algebra.polydiv]
q:296 [binder, in mathcomp.algebra.mxpoly]
q:298 [binder, in mathcomp.algebra.polydiv]
q:299 [binder, in mathcomp.field.closed_field]
q:3 [binder, in mathcomp.ssreflect.div]
q:300 [binder, in mathcomp.algebra.polydiv]
q:300 [binder, in mathcomp.algebra.mxpoly]
q:301 [binder, in mathcomp.ssreflect.div]
q:303 [binder, in mathcomp.algebra.polydiv]
q:304 [binder, in mathcomp.ssreflect.div]
q:304 [binder, in mathcomp.algebra.interval]
q:305 [binder, in mathcomp.algebra.polydiv]
q:306 [binder, in mathcomp.algebra.interval]
q:3063 [binder, in mathcomp.algebra.matrix]
q:307 [binder, in mathcomp.ssreflect.div]
q:308 [binder, in mathcomp.algebra.polydiv]
q:31 [binder, in mathcomp.algebra.polydiv]
q:311 [binder, in mathcomp.algebra.interval]
q:312 [binder, in mathcomp.algebra.polydiv]
q:3120 [binder, in mathcomp.algebra.matrix]
q:313 [binder, in mathcomp.algebra.interval]
q:314 [binder, in mathcomp.algebra.poly]
q:316 [binder, in mathcomp.algebra.poly]
q:318 [binder, in mathcomp.algebra.poly]
q:320 [binder, in mathcomp.algebra.poly]
q:322 [binder, in mathcomp.algebra.poly]
q:324 [binder, in mathcomp.algebra.poly]
q:327 [binder, in mathcomp.field.closed_field]
Q:327 [binder, in mathcomp.solvable.pgroup]
q:328 [binder, in mathcomp.field.closed_field]
Q:328 [binder, in mathcomp.solvable.pgroup]
q:329 [binder, in mathcomp.field.closed_field]
Q:329 [binder, in mathcomp.solvable.pgroup]
Q:33 [binder, in mathcomp.algebra.ring_quotient]
Q:330 [binder, in mathcomp.solvable.pgroup]
Q:331 [binder, in mathcomp.solvable.pgroup]
q:3321 [binder, in mathcomp.algebra.matrix]
q:3336 [binder, in mathcomp.algebra.matrix]
q:338 [binder, in mathcomp.field.algC]
q:340 [binder, in mathcomp.field.fieldext]
q:341 [binder, in mathcomp.field.fieldext]
q:3459 [binder, in mathcomp.ssreflect.order]
q:3461 [binder, in mathcomp.ssreflect.order]
q:3472 [binder, in mathcomp.ssreflect.order]
q:3474 [binder, in mathcomp.ssreflect.order]
q:348 [binder, in mathcomp.algebra.polydiv]
q:348 [binder, in mathcomp.field.fieldext]
q:35 [binder, in mathcomp.field.algebraics_fundamentals]
q:350 [binder, in mathcomp.algebra.polydiv]
q:350 [binder, in mathcomp.field.fieldext]
q:353 [binder, in mathcomp.algebra.polydiv]
q:354 [binder, in mathcomp.field.fieldext]
q:356 [binder, in mathcomp.algebra.polydiv]
q:359 [binder, in mathcomp.algebra.polydiv]
q:36 [binder, in mathcomp.algebra.polydiv]
q:365 [binder, in mathcomp.algebra.poly]
q:369 [binder, in mathcomp.field.fieldext]
q:370 [binder, in mathcomp.algebra.polydiv]
q:373 [binder, in mathcomp.algebra.polydiv]
q:374 [binder, in mathcomp.field.fieldext]
q:374 [binder, in mathcomp.field.closed_field]
q:375 [binder, in mathcomp.field.fieldext]
q:38 [binder, in mathcomp.ssreflect.div]
q:38 [binder, in mathcomp.algebra.polydiv]
q:382 [binder, in mathcomp.field.closed_field]
q:389 [binder, in mathcomp.field.closed_field]
Q:39 [binder, in mathcomp.algebra.ring_quotient]
q:390 [binder, in mathcomp.field.fieldext]
q:392 [binder, in mathcomp.algebra.intdiv]
q:392 [binder, in mathcomp.field.fieldext]
q:393 [binder, in mathcomp.field.fieldext]
q:393 [binder, in mathcomp.field.algnum]
q:394 [binder, in mathcomp.field.algnum]
q:395 [binder, in mathcomp.field.algnum]
Q:396 [binder, in mathcomp.ssreflect.ssrnat]
q:4 [binder, in mathcomp.ssreflect.choice]
q:40 [binder, in mathcomp.algebra.polydiv]
q:400 [binder, in mathcomp.algebra.polydiv]
Q:400 [binder, in mathcomp.ssreflect.ssrnat]
q:404 [binder, in mathcomp.algebra.mxpoly]
q:405 [binder, in mathcomp.algebra.intdiv]
q:405 [binder, in mathcomp.algebra.polydiv]
q:409 [binder, in mathcomp.algebra.polydiv]
q:410 [binder, in mathcomp.algebra.intdiv]
q:410 [binder, in mathcomp.algebra.polydiv]
q:412 [binder, in mathcomp.algebra.intdiv]
q:415 [binder, in mathcomp.algebra.intdiv]
q:415 [binder, in mathcomp.algebra.poly]
q:417 [binder, in mathcomp.algebra.intdiv]
q:419 [binder, in mathcomp.field.closed_field]
q:42 [binder, in mathcomp.algebra.intdiv]
Q:42 [binder, in mathcomp.solvable.sylow]
q:421 [binder, in mathcomp.algebra.intdiv]
q:428 [binder, in mathcomp.algebra.intdiv]
q:43 [binder, in mathcomp.algebra.polydiv]
q:430 [binder, in mathcomp.algebra.intdiv]
q:432 [binder, in mathcomp.algebra.polydiv]
q:435 [binder, in mathcomp.algebra.polydiv]
q:438 [binder, in mathcomp.algebra.polydiv]
q:439 [binder, in mathcomp.algebra.polydiv]
q:443 [binder, in mathcomp.algebra.polydiv]
q:449 [binder, in mathcomp.algebra.polydiv]
q:451 [binder, in mathcomp.algebra.polydiv]
q:453 [binder, in mathcomp.algebra.polydiv]
q:453 [binder, in mathcomp.algebra.poly]
q:455 [binder, in mathcomp.algebra.polydiv]
q:458 [binder, in mathcomp.algebra.polydiv]
Q:461 [binder, in mathcomp.ssreflect.bigop]
q:462 [binder, in mathcomp.algebra.polydiv]
q:471 [binder, in mathcomp.algebra.polydiv]
Q:48 [binder, in mathcomp.algebra.ring_quotient]
q:481 [binder, in mathcomp.algebra.polydiv]
q:485 [binder, in mathcomp.algebra.polydiv]
q:487 [binder, in mathcomp.algebra.polydiv]
q:489 [binder, in mathcomp.algebra.polydiv]
q:489 [binder, in mathcomp.algebra.poly]
q:49 [binder, in mathcomp.field.separable]
q:491 [binder, in mathcomp.algebra.polydiv]
q:493 [binder, in mathcomp.algebra.polydiv]
q:495 [binder, in mathcomp.algebra.poly]
q:496 [binder, in mathcomp.algebra.poly]
q:498 [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:502 [binder, in mathcomp.algebra.polydiv]
q:51 [binder, in mathcomp.solvable.alt]
q:51 [binder, in mathcomp.algebra.mxpoly]
q:52 [binder, in mathcomp.solvable.alt]
q:52 [binder, in mathcomp.algebra.polydiv]
q:531 [binder, in mathcomp.algebra.polydiv]
q:535 [binder, in mathcomp.algebra.polydiv]
q:539 [binder, in mathcomp.algebra.polydiv]
q:545 [binder, in mathcomp.algebra.polydiv]
Q:55 [binder, in mathcomp.solvable.sylow]
q:555 [binder, in mathcomp.algebra.polydiv]
q:557 [binder, in mathcomp.algebra.polydiv]
q:559 [binder, in mathcomp.algebra.polydiv]
q:568 [binder, in mathcomp.algebra.polydiv]
q:570 [binder, in mathcomp.algebra.polydiv]
q:575 [binder, in mathcomp.algebra.poly]
q:576 [binder, in mathcomp.algebra.polydiv]
q:577 [binder, in mathcomp.algebra.poly]
q:578 [binder, in mathcomp.algebra.mxalgebra]
q:579 [binder, in mathcomp.algebra.polydiv]
q:58 [binder, in mathcomp.algebra.polydiv]
q:58 [binder, in mathcomp.field.separable]
q:581 [binder, in mathcomp.algebra.polydiv]
q:581 [binder, in mathcomp.algebra.poly]
q:583 [binder, in mathcomp.algebra.poly]
q:585 [binder, in mathcomp.algebra.polydiv]
q:585 [binder, in mathcomp.algebra.mxalgebra]
q:588 [binder, in mathcomp.algebra.polydiv]
q:589 [binder, in mathcomp.algebra.polydiv]
Q:59 [binder, in mathcomp.solvable.sylow]
q:59 [binder, in mathcomp.algebra.poly]
q:591 [binder, in mathcomp.algebra.polydiv]
q:594 [binder, in mathcomp.algebra.polydiv]
q:596 [binder, in mathcomp.algebra.poly]
q:597 [binder, in mathcomp.algebra.polydiv]
q:599 [binder, in mathcomp.algebra.mxalgebra]
Q:6 [binder, in mathcomp.solvable.primitive_action]
Q:6 [binder, in mathcomp.algebra.ring_quotient]
q:60 [binder, in mathcomp.algebra.polydiv]
q:60 [binder, in mathcomp.algebra.polyXY]
q:600 [binder, in mathcomp.algebra.polydiv]
q:605 [binder, in mathcomp.algebra.polydiv]
q:606 [binder, in mathcomp.algebra.mxalgebra]
q:610 [binder, in mathcomp.algebra.polydiv]
q:613 [binder, in mathcomp.algebra.polydiv]
q:616 [binder, in mathcomp.algebra.polydiv]
q:619 [binder, in mathcomp.algebra.polydiv]
q:62 [binder, in mathcomp.algebra.polydiv]
q:620 [binder, in mathcomp.algebra.poly]
q:622 [binder, in mathcomp.algebra.polydiv]
q:622 [binder, in mathcomp.algebra.poly]
q:625 [binder, in mathcomp.algebra.polydiv]
q:625 [binder, in mathcomp.algebra.poly]
q:627 [binder, in mathcomp.algebra.poly]
q:628 [binder, in mathcomp.algebra.polydiv]
Q:63 [binder, in mathcomp.solvable.sylow]
q:631 [binder, in mathcomp.algebra.polydiv]
q:64 [binder, in mathcomp.algebra.polydiv]
q:64 [binder, in mathcomp.field.closed_field]
q:64 [binder, in mathcomp.algebra.poly]
q:643 [binder, in mathcomp.algebra.polydiv]
q:646 [binder, in mathcomp.algebra.polydiv]
q:664 [binder, in mathcomp.algebra.polydiv]
q:666 [binder, in mathcomp.algebra.polydiv]
q:67 [binder, in mathcomp.algebra.polyXY]
q:670 [binder, in mathcomp.algebra.polydiv]
q:670 [binder, in mathcomp.algebra.poly]
q:672 [binder, in mathcomp.algebra.poly]
q:673 [binder, in mathcomp.algebra.polydiv]
q:675 [binder, in mathcomp.algebra.poly]
q:676 [binder, in mathcomp.algebra.polydiv]
q:677 [binder, in mathcomp.algebra.poly]
q:679 [binder, in mathcomp.algebra.polydiv]
q:682 [binder, in mathcomp.algebra.polydiv]
q:684 [binder, in mathcomp.algebra.polydiv]
q:691 [binder, in mathcomp.algebra.polydiv]
q:699 [binder, in mathcomp.algebra.polydiv]
Q:7 [binder, in mathcomp.solvable.primitive_action]
q:7 [binder, in mathcomp.ssreflect.prime]
Q:70 [binder, in mathcomp.ssreflect.choice]
q:704 [binder, in mathcomp.algebra.polydiv]
q:706 [binder, in mathcomp.algebra.polydiv]
q:71 [binder, in mathcomp.algebra.mxpoly]
q:71 [binder, in mathcomp.algebra.polyXY]
q:712 [binder, in mathcomp.algebra.polydiv]
q:713 [binder, in mathcomp.algebra.polydiv]
q:716 [binder, in mathcomp.algebra.polydiv]
q:719 [binder, in mathcomp.algebra.polydiv]
q:721 [binder, in mathcomp.algebra.polydiv]
q:724 [binder, in mathcomp.algebra.polydiv]
q:726 [binder, in mathcomp.algebra.polydiv]
q:73 [binder, in mathcomp.algebra.polydiv]
q:73 [binder, in mathcomp.field.separable]
q:730 [binder, in mathcomp.algebra.polydiv]
q:733 [binder, in mathcomp.algebra.polydiv]
q:736 [binder, in mathcomp.algebra.polydiv]
q:738 [binder, in mathcomp.algebra.polydiv]
q:74 [binder, in mathcomp.algebra.polyXY]
q:741 [binder, in mathcomp.algebra.polydiv]
Q:75 [binder, in mathcomp.algebra.ring_quotient]
q:753 [binder, in mathcomp.algebra.polydiv]
q:755 [binder, in mathcomp.algebra.polydiv]
q:783 [binder, in mathcomp.ssreflect.path]
q:784 [binder, in mathcomp.ssreflect.path]
q:784 [binder, in mathcomp.algebra.poly]
q:789 [binder, in mathcomp.algebra.polydiv]
q:791 [binder, in mathcomp.algebra.poly]
q:792 [binder, in mathcomp.algebra.polydiv]
q:795 [binder, in mathcomp.algebra.polydiv]
q:796 [binder, in mathcomp.algebra.poly]
q:798 [binder, in mathcomp.algebra.polydiv]
Q:8 [binder, in mathcomp.solvable.primitive_action]
q:80 [binder, in mathcomp.field.algebraics_fundamentals]
q:80 [binder, in mathcomp.ssreflect.prime]
q:801 [binder, in mathcomp.ssreflect.order]
q:803 [binder, in mathcomp.algebra.polydiv]
q:803 [binder, in mathcomp.ssreflect.order]
q:805 [binder, in mathcomp.algebra.poly]
q:807 [binder, in mathcomp.ssreflect.order]
q:809 [binder, in mathcomp.algebra.polydiv]
q:809 [binder, in mathcomp.ssreflect.order]
q:81 [binder, in mathcomp.algebra.polyXY]
q:81 [binder, in mathcomp.algebra.fraction]
q:811 [binder, in mathcomp.algebra.polydiv]
q:815 [binder, in mathcomp.algebra.polydiv]
q:816 [binder, in mathcomp.algebra.poly]
q:817 [binder, in mathcomp.algebra.polydiv]
q:818 [binder, in mathcomp.algebra.polydiv]
q:819 [binder, in mathcomp.algebra.polydiv]
q:819 [binder, in mathcomp.algebra.poly]
q:820 [binder, in mathcomp.algebra.polydiv]
q:822 [binder, in mathcomp.algebra.polydiv]
q:823 [binder, in mathcomp.algebra.poly]
q:824 [binder, in mathcomp.algebra.polydiv]
q:828 [binder, in mathcomp.algebra.poly]
q:829 [binder, in mathcomp.algebra.polydiv]
q:829 [binder, in mathcomp.ssreflect.ssrnat]
q:83 [binder, in mathcomp.algebra.polydiv]
q:83 [binder, in mathcomp.algebra.mxpoly]
q:832 [binder, in mathcomp.algebra.poly]
q:833 [binder, in mathcomp.algebra.polydiv]
q:833 [binder, in mathcomp.ssreflect.ssrnat]
q:835 [binder, in mathcomp.algebra.polydiv]
q:837 [binder, in mathcomp.algebra.polydiv]
q:837 [binder, in mathcomp.ssreflect.ssrnat]
q:837 [binder, in mathcomp.algebra.poly]
Q:84 [binder, in mathcomp.algebra.ring_quotient]
q:840 [binder, in mathcomp.algebra.poly]
q:841 [binder, in mathcomp.algebra.polydiv]
q:841 [binder, in mathcomp.ssreflect.ssrnat]
q:842 [binder, in mathcomp.algebra.poly]
q:843 [binder, in mathcomp.algebra.polydiv]
q:850 [binder, in mathcomp.algebra.polydiv]
q:852 [binder, in mathcomp.algebra.polydiv]
q:855 [binder, in mathcomp.algebra.polydiv]
q:857 [binder, in mathcomp.algebra.polydiv]
q:86 [binder, in mathcomp.ssreflect.prime]
q:864 [binder, in mathcomp.algebra.polydiv]
q:866 [binder, in mathcomp.algebra.polydiv]
q:87 [binder, in mathcomp.algebra.mxpoly]
q:870 [binder, in mathcomp.algebra.polydiv]
q:870 [binder, in mathcomp.algebra.poly]
q:871 [binder, in mathcomp.algebra.poly]
q:872 [binder, in mathcomp.algebra.poly]
q:874 [binder, in mathcomp.algebra.polydiv]
q:874 [binder, in mathcomp.algebra.poly]
q:877 [binder, in mathcomp.algebra.poly]
q:878 [binder, in mathcomp.algebra.polydiv]
q:879 [binder, in mathcomp.algebra.polydiv]
q:88 [binder, in mathcomp.solvable.finmodule]
q:88 [binder, in mathcomp.field.fieldext]
q:88 [binder, in mathcomp.algebra.poly]
q:880 [binder, in mathcomp.algebra.poly]
q:882 [binder, in mathcomp.algebra.polydiv]
q:883 [binder, in mathcomp.algebra.poly]
q:886 [binder, in mathcomp.algebra.poly]
q:887 [binder, in mathcomp.algebra.polydiv]
q:889 [binder, in mathcomp.algebra.polydiv]
q:89 [binder, in mathcomp.algebra.polydiv]
q:89 [binder, in mathcomp.ssreflect.prime]
q:891 [binder, in mathcomp.algebra.polydiv]
q:893 [binder, in mathcomp.algebra.poly]
q:893 [binder, in mathcomp.algebra.mxalgebra]
q:894 [binder, in mathcomp.algebra.polydiv]
q:895 [binder, in mathcomp.algebra.poly]
q:899 [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.polyXY]
q:903 [binder, in mathcomp.algebra.polydiv]
q:904 [binder, in mathcomp.algebra.poly]
q:906 [binder, in mathcomp.algebra.polydiv]
q:909 [binder, in mathcomp.algebra.polydiv]
q:914 [binder, in mathcomp.algebra.poly]
q:922 [binder, in mathcomp.algebra.polydiv]
Q:923 [binder, in mathcomp.ssreflect.fintype]
q:925 [binder, in mathcomp.algebra.polydiv]
q:927 [binder, in mathcomp.algebra.polydiv]
Q:93 [binder, in mathcomp.ssreflect.choice]
q:93 [binder, in mathcomp.field.fieldext]
q:93 [binder, in mathcomp.algebra.poly]
q:931 [binder, in mathcomp.algebra.polydiv]
q:933 [binder, in mathcomp.algebra.polydiv]
q:935 [binder, in mathcomp.algebra.polydiv]
q:938 [binder, in mathcomp.algebra.polydiv]
q:94 [binder, in mathcomp.algebra.polyXY]
q:940 [binder, in mathcomp.algebra.polydiv]
q:942 [binder, in mathcomp.algebra.polydiv]
q:945 [binder, in mathcomp.algebra.polydiv]
q:946 [binder, in mathcomp.algebra.poly]
q:948 [binder, in mathcomp.algebra.polydiv]
q:95 [binder, in mathcomp.algebra.polydiv]
q:95 [binder, in mathcomp.field.closed_field]
q:959 [binder, in mathcomp.algebra.polydiv]
q:96 [binder, in mathcomp.algebra.polydiv]
q:96 [binder, in mathcomp.field.fieldext]
q:962 [binder, in mathcomp.algebra.polydiv]
q:965 [binder, in mathcomp.algebra.polydiv]
q:971 [binder, in mathcomp.algebra.polydiv]
q:976 [binder, in mathcomp.algebra.polydiv]
q:979 [binder, in mathcomp.algebra.poly]
q:98 [binder, in mathcomp.field.closed_field]
q:98 [binder, in mathcomp.algebra.polyXY]
q:980 [binder, in mathcomp.algebra.polydiv]
q:982 [binder, in mathcomp.algebra.poly]
q:983 [binder, in mathcomp.algebra.polydiv]
q:985 [binder, in mathcomp.algebra.poly]
q:986 [binder, in mathcomp.algebra.polydiv]
q:987 [binder, in mathcomp.algebra.poly]
q:988 [binder, in mathcomp.algebra.polydiv]
q:989 [binder, in mathcomp.algebra.poly]
q:99 [binder, in mathcomp.field.fieldext]
q:990 [binder, in mathcomp.algebra.polydiv]
q:992 [binder, in mathcomp.algebra.polydiv]
q:994 [binder, in mathcomp.algebra.polydiv]
q:996 [binder, in mathcomp.algebra.polydiv]

Global Index

_

(75489 entries)

Notation Index

H

J

T

W

X

Y

_

(1813 entries)

Binder Index

_

other

(45320 entries)

Module Index

H

J

K

L

W

X

Y

Z

_

other

(382 entries)

Variable Index

J

W

X

Y

_

other

(3967 entries)

Library Index

K

L

U

W

X

Y

_

other

(91 entries)

Lemma Index

Y

_

other

(14046 entries)

Constructor Index

J

K

W

Y

_

other

(469 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(128 entries)

Projection Index

H

J

K

L

W

X

Y

_

other

(457 entries)

Section Index

J

W

X

Y

_

other

(1372 entries)

Abbreviation Index

Y

_

other

(1025 entries)

Definition Index

Y

_

other

(6124 entries)

Record Index

H

J

K

L

W

X

Y

_

other

(250 entries)