mathcomp.ssreflect.tuple

Global Index

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 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]
qfpoly [definition, in mathcomp.field.qfpoly]
qfpoly [library]
qfpoly_splitting_field_type [definition, in mathcomp.field.qfpoly]
qfpoly_const [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_Field [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_IntegralDomain [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_ComUnitRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_ComRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_UnitAlgebra [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_UnitRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_Algebra [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_Lalgebra [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_Lmodule [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_ComSemiRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_Field [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_IntegralDomain [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_ComUnitRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_ComRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_UnitRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_ComSemiRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__fieldext_FieldExt [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__falgebra_Falgebra [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__vector_Vector [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_ComUnitAlgebra [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_UnitAlgebra [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_ComAlgebra [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_Algebra [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_Lalgebra [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_Lmodule [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_Field [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_IntegralDomain [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_ComUnitRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_UnitRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_ComRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_ComSemiRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_Ring [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_Zmodule [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_SemiRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__FinRing_Nmodule [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__fintype_Finite [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_Ring [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_Zmodule [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_SemiRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__CountRing_Nmodule [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__choice_Countable [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_Ring [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_Zmodule [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_SemiRing [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__GRing_Nmodule [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__choice_Choice [definition, in mathcomp.field.qfpoly]
qfpoly_qfpoly__canonical__eqtype_Equality [definition, in mathcomp.field.qfpoly]
qf_eval [abbreviation, in mathcomp.character.mxrepresentation]
qf_form [abbreviation, in mathcomp.character.mxrepresentation]
qidmx [definition, in mathcomp.algebra.mxalgebra]
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_dvd [lemma, in mathcomp.algebra.intdiv]
Qn_aut_exists [lemma, in mathcomp.field.algnum]
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_qpoly__canonical__FinRing_ComUnitRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_ComRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_UnitAlgebra [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_UnitRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_Algebra [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_Lalgebra [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_Ring [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_Lmodule [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_Zmodule [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_ComSemiRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_SemiRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__FinRing_Nmodule [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__fintype_Finite [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__CountRing_ComUnitRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__CountRing_ComRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__CountRing_UnitRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__CountRing_Ring [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__CountRing_Zmodule [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__CountRing_ComSemiRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__CountRing_SemiRing [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__CountRing_Nmodule [definition, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__choice_Countable [definition, in mathcomp.field.qfpoly]
qpoly_inv0 [lemma, in mathcomp.field.qfpoly]
qpoly_mulVp [lemma, in mathcomp.field.qfpoly]
qpoly_qpoly__canonical__GRing_ComUnitAlgebra [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_ComUnitRing [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_UnitAlgebra [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_UnitRing [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_ComUnitAlgebra [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_ComUnitRing [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_UnitAlgebra [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_UnitRing [definition, in mathcomp.algebra.qpoly]
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_qpoly__canonical__GRing_ComAlgebra [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_Algebra [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_ComAlgebra [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_Algebra [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_Lalgebra [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_Lmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_Lalgebra [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_qpolyC__canonical__GRing_RMorphism [definition, in mathcomp.algebra.qpoly]
qpoly_qpolyC__canonical__GRing_Additive [definition, in mathcomp.algebra.qpoly]
qpoly_in_qpoly__canonical__GRing_LRMorphism [definition, in mathcomp.algebra.qpoly]
qpoly_in_qpoly__canonical__GRing_RMorphism [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_ComRing [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_ComSemiRing [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_Ring [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_SemiRing [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_Zmodule [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__GRing_Nmodule [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__choice_Choice [definition, in mathcomp.algebra.qpoly]
qpoly_qpoly__canonical__eqtype_Equality [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_ComRing [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_ComSemiRing [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_Ring [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_SemiRing [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_in_qpoly__canonical__GRing_Linear [definition, in mathcomp.algebra.qpoly]
qpoly_in_qpoly__canonical__GRing_Additive [definition, in mathcomp.algebra.qpoly]
qpoly_polyn__canonical__GRing_Linear [definition, in mathcomp.algebra.qpoly]
qpoly_polyn__canonical__GRing_Additive [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__fintype_SubFinite [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__FinRing_Lmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__FinRing_Zmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__FinRing_Nmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__fintype_Finite [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__choice_SubCountable [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__CountRing_Zmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__CountRing_Nmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__choice_Countable [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__vector_Vector [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_SubLmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_SubZmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_SubNmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_Lmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_Zmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__GRing_Nmodule [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__choice_SubChoice [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__eqtype_SubEquality [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__choice_Choice [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__eqtype_Equality [definition, in mathcomp.algebra.qpoly]
qpoly_npoly__canonical__eqtype_SubType [definition, in mathcomp.algebra.qpoly]
qpoly_poly_of_size_pred__canonical__GRing_SubmodClosed [definition, in mathcomp.algebra.qpoly]
qpoly_poly_of_size_pred__canonical__GRing_ZmodClosed [definition, in mathcomp.algebra.qpoly]
qpoly_poly_of_size_pred__canonical__GRing_AddClosed [definition, in mathcomp.algebra.qpoly]
qpoly_poly_of_size_pred__canonical__GRing_OppClosed [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]
QRing [section, in mathcomp.algebra.qpoly]
QRing.A [variable, in mathcomp.algebra.qpoly]
QRing.h [variable, in mathcomp.algebra.qpoly]
qT [abbreviation, in mathcomp.field.qfpoly]
QtoC [abbreviation, in mathcomp.field.cyclotomic]
QtoC [abbreviation, in mathcomp.field.algC]
QtoC [abbreviation, in mathcomp.field.algnum]
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_gtype_unlock_subterm [definition, in mathcomp.solvable.extremal]
quaternion_gtype.unlock [definition, in mathcomp.solvable.extremal]
quaternion_gtype.body [definition, in mathcomp.solvable.extremal]
quaternion_gtype [module, in mathcomp.solvable.extremal]
quaternion_gtype_Locked.unlock [axiom, in mathcomp.solvable.extremal]
quaternion_gtype_Locked.body [axiom, in mathcomp.solvable.extremal]
quaternion_gtype_Locked [module, 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.ssreflect.generic_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]
QuotientElpiOperations [module, in mathcomp.ssreflect.generic_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_coset_of__canonical__fingroup_FinGroup [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__fingroup_BaseFinGroup [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__fintype_SubFinite [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__fintype_Finite [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__choice_SubCountable [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__choice_SubChoice [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__eqtype_SubEquality [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__choice_Countable [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__choice_Choice [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__eqtype_Equality [definition, in mathcomp.fingroup.quotient]
quotient_coset_of__canonical__eqtype_SubType [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.axioms_ [record, in mathcomp.ssreflect.generic_quotient]
Quotient.choice_Choice__to__choice_hasChoice [definition, in mathcomp.algebra.ring_quotient]
Quotient.class [projection, in mathcomp.ssreflect.generic_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.ssreflect.generic_quotient]
Quotient.Exports [module, in mathcomp.algebra.ring_quotient]
Quotient.generic_quotient_isQuotient_mixin [projection, in mathcomp.ssreflect.generic_quotient]
Quotient.generic_quotient_EqQuotient__to__generic_quotient_isEqQuotient [definition, in mathcomp.algebra.ring_quotient]
Quotient.generic_quotient_EqQuotient__to__eqtype_hasDecEq [definition, in mathcomp.algebra.ring_quotient]
Quotient.generic_quotient_EqQuotient__to__generic_quotient_isQuotient [definition, in mathcomp.algebra.ring_quotient]
Quotient.GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing [definition, in mathcomp.algebra.ring_quotient]
Quotient.GRing_Zmodule_isComRing__to__GRing_SemiRing_hasCommutativeMul [definition, in mathcomp.algebra.ring_quotient]
Quotient.GRing_isZmodule__to__GRing_isNmodule [definition, in mathcomp.algebra.ring_quotient]
Quotient.GRing_isZmodule__to__GRing_Nmodule_isZmodule [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_factory_37 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_mixin_36 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_mixin_35 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_factory_32 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_factory_30 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_mixin_29 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_mixin_28 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_factory_25 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_mixin_24 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_factory_21 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_mixin_20 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_mixin_19 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_mixin_18 [definition, in mathcomp.algebra.ring_quotient]
Quotient.HB_unnamed_factory_14 [definition, 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.pack_ [definition, in mathcomp.ssreflect.generic_quotient]
Quotient.phant_on_ [definition, in mathcomp.ssreflect.generic_quotient]
Quotient.phant_clone [definition, in mathcomp.ssreflect.generic_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.Quotient_quot__canonical__ring_quotient_RingQuotient [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__GRing_ComRing [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__GRing_ComSemiRing [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__GRing_Ring [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__GRing_SemiRing [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__ring_quotient_ZmodQuotient [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__GRing_Zmodule [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__GRing_Nmodule [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__choice_Choice [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__generic_quotient_EqQuotient [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__eqtype_Equality [definition, in mathcomp.algebra.ring_quotient]
Quotient.Quotient_quot__canonical__generic_quotient_Quotient [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.sort [projection, in mathcomp.ssreflect.generic_quotient]
Quotient.type [record, in mathcomp.ssreflect.generic_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.eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.Exports [module, in mathcomp.ssreflect.generic_quotient]
QuotSubType.generic_quotient_quot_type_of__canonical__eqtype_SubEquality [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.generic_quotient_quot_type_of__canonical__eqtype_Equality [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.generic_quotient_quot_type_of__canonical__eqtype_SubType [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.HB_unnamed_mixin_9 [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.HB_unnamed_factory_7 [definition, in mathcomp.ssreflect.generic_quotient]
QuotSubType.HB_unnamed_factory_5 [definition, 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 [definition, 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]
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]
Q8_extraspecial [lemma, in mathcomp.solvable.extraspecial]

Global Index

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 entries)