A (Abbreviations)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
A (Abbreviations)
a [abbrev, in mathcomp.group_representation.integral_char]a [abbrev, in mathcomp.group_representation.integral_char]
A' [abbrev, in mathcomp.solvable.hall]
ab_rV_P [abbrev, in mathcomp.group_representation.mxabelem]
AC [abbrev, in mathcomp.boot.ssrAC]
AC_check_pattern [abbrev, in mathcomp.boot.ssrAC]
AC_strategy [abbrev, in mathcomp.boot.ssrAC]
ACl [abbrev, in mathcomp.boot.ssrAC]
ACof [abbrev, in mathcomp.boot.ssrAC]
actp [abbrev, in mathcomp.solvable.extraspecial]
actT [abbrev, in mathcomp.finite_group.action]
Ad [abbrev, in mathcomp.algebra.mxpoly]
addsmx [abbrev, in mathcomp.algebra.mxalgebra]
addV [abbrev, in mathcomp.algebra.vector]
aG [abbrev, in mathcomp.group_representation.mxrepresentation]
aG [abbrev, in mathcomp.group_representation.mxrepresentation]
algC'G [abbrev, in mathcomp.group_representation.classfun]
algC_pfactor [abbrev, in mathcomp.field.algC]
Algebra.AddClosed [abbrev, in mathcomp.boot.nmodule]
Algebra.AddClosed.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.AddClosed.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.AddClosed.Exports.addrClosed [abbrev, in mathcomp.boot.nmodule]
Algebra.AddClosed.on [abbrev, in mathcomp.boot.nmodule]
Algebra.AddClosed.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.Additive [abbrev, in mathcomp.boot.nmodule]
Algebra.Additive.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.Additive.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.Additive.on [abbrev, in mathcomp.boot.nmodule]
Algebra.Additive.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.AddMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.AddMagma.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.AddMagma.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.AddMagma.Exports.addMagmaType [abbrev, in mathcomp.boot.nmodule]
Algebra.AddMagma.on [abbrev, in mathcomp.boot.nmodule]
Algebra.AddMagma.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.AddMagma_isAddSemigroup [abbrev, in mathcomp.boot.nmodule]
Algebra.AddMagma_isAddSemigroup.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.AddMagma_isAddSemigroup.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.AddSemigroup [abbrev, in mathcomp.boot.nmodule]
Algebra.AddSemigroup.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.AddSemigroup.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.AddSemigroup.Exports.addSemigroupType [abbrev, in mathcomp.boot.nmodule]
Algebra.AddSemigroup.on [abbrev, in mathcomp.boot.nmodule]
Algebra.AddSemigroup.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.AddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.AddUMagma.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.AddUMagma.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.AddUMagma.Exports.addUMagmaType [abbrev, in mathcomp.boot.nmodule]
Algebra.AddUMagma.on [abbrev, in mathcomp.boot.nmodule]
Algebra.AddUMagma.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma.Exports.baseAddMagmaType [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma.on [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma_isAddMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma_isAddMagma.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma_isAddMagma.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma.Exports.baseAddUMagmaType [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma.on [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma_isAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma_isAddUMagma.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma_isAddUMagma.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseZmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseZmodule.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseZmodule.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseZmodule.Exports.baseZmodType [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseZmodule.on [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseZmodule.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseZmoduleNmodule_isZmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseZmoduleNmodule_isZmodule.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.BaseZmoduleNmodule_isZmodule.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_13.add [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_13.addrC [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_20.add [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_20.addrA [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_20.addrC [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_43.add [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_43.add0r [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_43.addrC [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_43.zero [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_58.add [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_58.add0r [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_58.addrA [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_58.addrC [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_58.zero [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_74.addNr [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_74.opp [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_81.add [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_81.add0r [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_81.addNr [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_81.addrA [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_81.addrC [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_81.opp [abbrev, in mathcomp.boot.nmodule]
Algebra.Builders_81.zero [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma.on [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.on [abbrev, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.hasAdd [abbrev, in mathcomp.boot.nmodule]
Algebra.hasAdd.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.hasAdd.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.hasOpp [abbrev, in mathcomp.boot.nmodule]
Algebra.hasOpp.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.hasOpp.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.hasZero [abbrev, in mathcomp.boot.nmodule]
Algebra.hasZero.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.hasZero.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddClosed [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddClosed.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddClosed.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isAdditive.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddMagma.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddMagma.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddSemigroup [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddSemigroup.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddSemigroup.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddUMagma.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isAddUMagma.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isNmodMorphism [abbrev, in mathcomp.boot.nmodule]
Algebra.isNmodMorphism.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isNmodMorphism.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isNmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.isNmodule.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isNmodule.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isOppClosed [abbrev, in mathcomp.boot.nmodule]
Algebra.isOppClosed.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isOppClosed.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isSemiAdditive.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isSubBaseAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.isSubBaseAddUMagma.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isSubBaseAddUMagma.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isSubZmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.isSubZmodule.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isSubZmodule.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isZmodClosed [abbrev, in mathcomp.boot.nmodule]
Algebra.isZmodClosed.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isZmodClosed.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isZmodMorphism [abbrev, in mathcomp.boot.nmodule]
Algebra.isZmodMorphism.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isZmodMorphism.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.isZmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.isZmodule.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.isZmodule.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.MathCompCompatAdditive.Additive.axiom [abbrev, in mathcomp.boot.nmodule]
Algebra.MathCompCompatAdditive.Additive.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.MathCompCompatAdditive.Additive.class_of [abbrev, in mathcomp.boot.nmodule]
Algebra.MathCompCompatAdditive.Additive.mcpack [abbrev, in mathcomp.boot.nmodule]
Algebra.MathCompCompatAdditive.Additive.Mixin [abbrev, in mathcomp.boot.nmodule]
Algebra.MathCompCompatAdditive.Additive.mixin_of [abbrev, in mathcomp.boot.nmodule]
Algebra.nmod_closed [abbrev, in mathcomp.boot.nmodule]
Algebra.Nmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.Nmodule.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.Nmodule.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.Nmodule.Exports.nmodType [abbrev, in mathcomp.boot.nmodule]
Algebra.Nmodule.on [abbrev, in mathcomp.boot.nmodule]
Algebra.Nmodule.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.Nmodule_isZmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.Nmodule_isZmodule.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.Nmodule_isZmodule.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.OppClosed [abbrev, in mathcomp.boot.nmodule]
Algebra.OppClosed.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.OppClosed.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.OppClosed.Exports.opprClosed [abbrev, in mathcomp.boot.nmodule]
Algebra.OppClosed.on [abbrev, in mathcomp.boot.nmodule]
Algebra.OppClosed.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.Exports.subAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.on [abbrev, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.subBaseAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.on [abbrev, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubAddUMagma [abbrev, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubAddUMagma.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubAddUMagma.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubNmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubNmodule.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubNmodule.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubZmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubZmodule.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubZmodule.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.SubNmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.SubNmodule.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.SubNmodule.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.subNmodType [abbrev, in mathcomp.boot.nmodule]
Algebra.SubNmodule.on [abbrev, in mathcomp.boot.nmodule]
Algebra.SubNmodule.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.SubNmodule_isSubZmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.SubNmodule_isSubZmodule.axioms [abbrev, in mathcomp.boot.nmodule]
Algebra.SubNmodule_isSubZmodule.Build [abbrev, in mathcomp.boot.nmodule]
Algebra.SubZmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.SubZmodule.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.SubZmodule.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.subZmodType [abbrev, in mathcomp.boot.nmodule]
Algebra.SubZmodule.on [abbrev, in mathcomp.boot.nmodule]
Algebra.SubZmodule.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.val [abbrev, in mathcomp.boot.nmodule]
Algebra.val [abbrev, in mathcomp.boot.nmodule]
Algebra.ZmodClosed [abbrev, in mathcomp.boot.nmodule]
Algebra.ZmodClosed.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.ZmodClosed.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.ZmodClosed.Exports.zmodClosed [abbrev, in mathcomp.boot.nmodule]
Algebra.ZmodClosed.on [abbrev, in mathcomp.boot.nmodule]
Algebra.ZmodClosed.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra.Zmodule [abbrev, in mathcomp.boot.nmodule]
Algebra.Zmodule.clone [abbrev, in mathcomp.boot.nmodule]
Algebra.Zmodule.copy [abbrev, in mathcomp.boot.nmodule]
Algebra.Zmodule.Exports.zmodType [abbrev, in mathcomp.boot.nmodule]
Algebra.Zmodule.on [abbrev, in mathcomp.boot.nmodule]
Algebra.Zmodule.on_ [abbrev, in mathcomp.boot.nmodule]
Algebra_isFalgebra [abbrev, in mathcomp.field.falgebra]
Algebra_isFalgebra.axioms [abbrev, in mathcomp.field.falgebra]
Algebra_isFalgebra.Build [abbrev, in mathcomp.field.falgebra]
Algebraics.Exports.algC [abbrev, in mathcomp.field.algC]
Algebraics.Exports.algCeq [abbrev, in mathcomp.field.algC]
Algebraics.Exports.algCfield [abbrev, in mathcomp.field.algC]
Algebraics.Exports.algCnum [abbrev, in mathcomp.field.algC]
Algebraics.Exports.algCnumClosedField [abbrev, in mathcomp.field.algC]
Algebraics.Exports.algCnumField [abbrev, in mathcomp.field.algC]
Algebraics.Exports.algCnzRing [abbrev, in mathcomp.field.algC]
Algebraics.Exports.algCring [abbrev, in mathcomp.field.algC]
Algebraics.Exports.algCuring [abbrev, in mathcomp.field.algC]
Algebraics.Exports.algCzmod [abbrev, in mathcomp.field.algC]
Algebraics.Exports.Creal [abbrev, in mathcomp.field.algC]
Algebraics.Implementation.cfType [abbrev, in mathcomp.field.algC]
Algebraics.Implementation.pQtoL [abbrev, in mathcomp.field.algC]
Algebraics.Internals.algC [abbrev, in mathcomp.field.algC]
Algebraics.Internals.pQtoC [abbrev, in mathcomp.field.algC]
Algebraics.Internals.QtoC [abbrev, in mathcomp.field.algC]
algType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
all2rel [abbrev, in mathcomp.boot.seq]
all_comm_mx [abbrev, in mathcomp.algebra.matrix]
all_comm_mx [abbrev, in mathcomp.algebra.matrix]
all_similar_to [abbrev, in mathcomp.algebra.mxred]
all_simmx_in [abbrev, in mathcomp.algebra.mxpoly]
And [abbrev, in mathcomp.group_representation.mxrepresentation]
applyr [abbrev, in mathcomp.algebra.sesquilinear]
archiDomainType [abbrev, in mathcomp.algebra.archimedean]
archiFieldType [abbrev, in mathcomp.algebra.archimedean]
AtoB [abbrev, in mathcomp.group_representation.inertia]