A (Definitions)

Files

K

U

W

X

Y

_

Definitions

Y

_

Lemmas

Y

_

Abbreviations

Y

_

Global Index

Y

_

A (Definitions)

abelem [def, in mathcomp.solvable.abelian]
abelem_dim' [def, in mathcomp.group_representation.mxabelem]
abelem_mx [def, in mathcomp.group_representation.mxabelem]
abelem_mx_fun [def, in mathcomp.group_representation.mxabelem]
abelem_repr [def, in mathcomp.group_representation.mxabelem]
abelem_rV [def, in mathcomp.group_representation.mxabelem]
abelem_rV_morphism [def, in mathcomp.group_representation.mxabelem]
abelian [def, in mathcomp.finite_group.fingroup]
abelian_type [def, in mathcomp.solvable.abelian]
abelian_type_rec [def, in mathcomp.solvable.abelian]
absz [def, in mathcomp.algebra.ssrint]
AC.cforall [def, in mathcomp.boot.ssrAC]
AC.content [def, in mathcomp.boot.ssrAC]
AC.direct [def, in mathcomp.boot.ssrAC]
AC.eval [def, in mathcomp.boot.ssrAC]
AC.Leaf_of_nat [def, in mathcomp.boot.ssrAC]
AC.pattern [def, in mathcomp.boot.ssrAC]
AC.pos [def, in mathcomp.boot.ssrAC]
AC.serial [def, in mathcomp.boot.ssrAC]
AC.set_pos [def, in mathcomp.boot.ssrAC]
AC.set_pos_trec [def, in mathcomp.boot.ssrAC]
AC.unzip [def, in mathcomp.boot.ssrAC]
acomps [def, in mathcomp.solvable.jordanholder]
act_dom [def, in mathcomp.finite_group.action]
act_f [def, in mathcomp.solvable.burnside_app]
act_g [def, in mathcomp.solvable.burnside_app]
act_morph [def, in mathcomp.finite_group.action]
act_morphism [def, in mathcomp.finite_group.action]
actby [def, in mathcomp.finite_group.action]
actby_cond [def, in mathcomp.finite_group.action]
actby_cond_group [def, in mathcomp.finite_group.action]
actby_groupAction [def, in mathcomp.finite_group.action]
action_by [def, in mathcomp.finite_group.action]
actm [def, in mathcomp.finite_group.action]
actperm [def, in mathcomp.finite_group.action]
actperm_morphism [def, in mathcomp.finite_group.action]
acts_irreducibly [def, in mathcomp.finite_group.action]
acts_on [def, in mathcomp.finite_group.action]
acts_on_group [def, in mathcomp.finite_group.action]
add0mx [def, in mathcomp.algebra.matrix]
add_lfun [def, in mathcomp.algebra.vector]
add_pair [def, in mathcomp.boot.nmodule]
add_poly [def, in mathcomp.algebra.poly]
add_poly_def [def, in mathcomp.algebra.poly]
add_poly_unlockable [def, in mathcomp.algebra.poly]
addmx [def, in mathcomp.algebra.matrix]
addmxA [def, in mathcomp.algebra.matrix]
addmxC [def, in mathcomp.algebra.matrix]
addn [def, in mathcomp.boot.ssrnat]
addn_rec [def, in mathcomp.boot.ssrnat]
addq [def, in mathcomp.algebra.rat]
addq_subdef [def, in mathcomp.algebra.rat]
addsmx.body [def, in mathcomp.algebra.mxalgebra]
addsmx.unlock [def, in mathcomp.algebra.mxalgebra]
addsmx_nop [def, in mathcomp.algebra.mxalgebra]
addsmx_unlock_subterm [def, in mathcomp.algebra.mxalgebra]
addsmx_unlockable [def, in mathcomp.algebra.mxalgebra]
addv [def, in mathcomp.algebra.vector]
addv_pi1 [def, in mathcomp.algebra.vector]
addv_pi2 [def, in mathcomp.algebra.vector]
adhoc_seq_sub_choiceType [def, in mathcomp.boot.fintype]
adhoc_seq_sub_countType [def, in mathcomp.boot.fintype]
adhoc_seq_sub_finType [def, in mathcomp.boot.fintype]
adjoin_degree [def, in mathcomp.field.fieldext]
adjugate [def, in mathcomp.algebra.matrix]
AEnd_FinGroup.comp_AEnd [def, in mathcomp.field.galois]
AEnd_FinGroup.inAEnd [def, in mathcomp.field.galois]
AEnd_FinGroup.kAEnd [def, in mathcomp.field.galois]
AEnd_FinGroup.kAEnd_group [def, in mathcomp.field.galois]
AEnd_FinGroup.kAEndf [def, in mathcomp.field.galois]
AEnd_FinGroup.kAEndf_group [def, in mathcomp.field.galois]
afix [def, in mathcomp.finite_group.action]
agenv [def, in mathcomp.field.falgebra]
agenv_aspace [def, in mathcomp.field.falgebra]
ahom_in [def, in mathcomp.field.falgebra]
ahom_is_multiplicative [def, in mathcomp.field.falgebra]
aimg_aspace [def, in mathcomp.field.fieldext]
Aint [def, in mathcomp.field.algnum]
algC_algebraic [def, in mathcomp.field.algC]
algC_intr_inj [def, in mathcomp.field.cyclotomic]
algC_invaut [def, in mathcomp.field.algC]
algC_invaut_is_additive [def, in mathcomp.field.algC]
algC_invaut_is_multiplicative [def, in mathcomp.field.algC]
Algebra.add [def, in mathcomp.boot.nmodule]
Algebra.add0r [def, in mathcomp.boot.nmodule]
Algebra.add_fun [def, in mathcomp.boot.nmodule]
Algebra.AddClosed.pack_ [def, in mathcomp.boot.nmodule]
Algebra.AddClosed.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.AddClosed.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.additive [def, in mathcomp.boot.nmodule]
Algebra.Additive.pack_ [def, in mathcomp.boot.nmodule]
Algebra.Additive.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.Additive.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.AddMagma.pack_ [def, in mathcomp.boot.nmodule]
Algebra.AddMagma.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.AddMagma.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.AddMagma_isAddSemigroup.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.AddMagma_isAddSemigroup.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.AddMagma_isAddSemigroup.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.addNr [def, in mathcomp.boot.nmodule]
Algebra.addr_closed [def, in mathcomp.boot.nmodule]
Algebra.addrA [def, in mathcomp.boot.nmodule]
Algebra.addrC [def, in mathcomp.boot.nmodule]
Algebra.AddSemigroup.pack_ [def, in mathcomp.boot.nmodule]
Algebra.AddSemigroup.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.AddSemigroup.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.AddUMagma.Exports.join_Algebra_AddUMagma_between_Algebra_AddMagma_and_Algebra_BaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.AddUMagma.Exports.join_Algebra_AddUMagma_between_Algebra_AddMagma_and_Algebra_ChoiceBaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.AddUMagma.pack_ [def, in mathcomp.boot.nmodule]
Algebra.AddUMagma.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.AddUMagma.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.addumagma_closed [def, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma.pack_ [def, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma_isAddMagma.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma_isAddMagma.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.BaseAddMagma_isAddMagma.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma.pack_ [def, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma_isAddUMagma.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma_isAddUMagma.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.BaseAddUMagma_isAddUMagma.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.BaseZmodule.pack_ [def, in mathcomp.boot.nmodule]
Algebra.BaseZmodule.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.BaseZmodule.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.BaseZmoduleNmodule_isZmodule.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.BaseZmoduleNmodule_isZmodule.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.BaseZmoduleNmodule_isZmodule.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.can2_additive [def, in mathcomp.boot.nmodule]
Algebra.can2_semi_additive [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma.Exports.join_Algebra_ChoiceBaseAddMagma_between_Algebra_BaseAddMagma_and_choice_Choice [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma.Exports.join_Algebra_ChoiceBaseAddMagma_between_Algebra_BaseAddMagma_and_eqtype_Equality [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma.pack_ [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddMagma.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.Exports.join_Algebra_ChoiceBaseAddUMagma_between_Algebra_BaseAddUMagma_and_Algebra_ChoiceBaseAddMagma [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.Exports.join_Algebra_ChoiceBaseAddUMagma_between_Algebra_BaseAddUMagma_and_choice_Choice [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.Exports.join_Algebra_ChoiceBaseAddUMagma_between_Algebra_BaseAddUMagma_and_eqtype_Equality [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.pack_ [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.ChoiceBaseAddUMagma.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.hasAdd.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.hasAdd.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.hasAdd.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.hasOpp.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.hasOpp.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.hasOpp.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.hasZero.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.hasZero.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.hasZero.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isAddClosed.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.isAddClosed.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isAddClosed.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isAddMagma.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isAddMagma.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isAddSemigroup.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isAddSemigroup.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isAddUMagma.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isAddUMagma.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isNmodMorphism.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.isNmodMorphism.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isNmodMorphism.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isNmodule.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isNmodule.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isOppClosed.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.isOppClosed.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isOppClosed.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isSubBaseAddUMagma.identity_builder [def, in mathcomp.boot.nmodule]
Algebra.isSubBaseAddUMagma.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isSubBaseAddUMagma.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isSubZmodule.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isSubZmodule.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isZmodClosed.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isZmodClosed.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isZmodMorphism.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isZmodMorphism.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.isZmodule.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.isZmodule.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.MathCompCompatAdditive.Additive.phant_mcpack [def, in mathcomp.boot.nmodule]
Algebra.natmul [def, in mathcomp.boot.nmodule]
Algebra.nmod_morphism [def, in mathcomp.boot.nmodule]
Algebra.Nmodule.Exports.join_Algebra_Nmodule_between_Algebra_AddSemigroup_and_Algebra_AddUMagma [def, in mathcomp.boot.nmodule]
Algebra.Nmodule.Exports.join_Algebra_Nmodule_between_Algebra_AddSemigroup_and_Algebra_BaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.Nmodule.Exports.join_Algebra_Nmodule_between_Algebra_AddSemigroup_and_Algebra_ChoiceBaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.Nmodule.pack_ [def, in mathcomp.boot.nmodule]
Algebra.Nmodule.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.Nmodule.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.Nmodule_isZmodule.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.Nmodule_isZmodule.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.null_fun [def, in mathcomp.boot.nmodule]
Algebra.opp [def, in mathcomp.boot.nmodule]
Algebra.opp_fun [def, in mathcomp.boot.nmodule]
Algebra.OppClosed.pack_ [def, in mathcomp.boot.nmodule]
Algebra.OppClosed.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.OppClosed.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.oppr_closed [def, in mathcomp.boot.nmodule]
Algebra.semi_additive [def, in mathcomp.boot.nmodule]
Algebra.sub_fun [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.Exports.join_Algebra_SubAddUMagma_between_Algebra_AddMagma_and_Algebra_SubBaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.Exports.join_Algebra_SubAddUMagma_between_Algebra_AddMagma_and_choice_SubChoice [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.Exports.join_Algebra_SubAddUMagma_between_Algebra_AddMagma_and_eqtype_SubEquality [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.Exports.join_Algebra_SubAddUMagma_between_Algebra_AddMagma_and_eqtype_SubType [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.Exports.join_Algebra_SubAddUMagma_between_Algebra_AddUMagma_and_Algebra_SubBaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.Exports.join_Algebra_SubAddUMagma_between_Algebra_AddUMagma_and_choice_SubChoice [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.Exports.join_Algebra_SubAddUMagma_between_Algebra_AddUMagma_and_eqtype_SubEquality [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.Exports.join_Algebra_SubAddUMagma_between_Algebra_AddUMagma_and_eqtype_SubType [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.pack_ [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.SubAddUMagma.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_BaseAddMagma_and_choice_SubChoice [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_BaseAddMagma_and_eqtype_SubEquality [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_BaseAddMagma_and_eqtype_SubType [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_BaseAddUMagma_and_choice_SubChoice [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_BaseAddUMagma_and_eqtype_SubEquality [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_BaseAddUMagma_and_eqtype_SubType [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_ChoiceBaseAddMagma_and_choice_SubChoice [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_ChoiceBaseAddMagma_and_eqtype_SubEquality [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_ChoiceBaseAddMagma_and_eqtype_SubType [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_ChoiceBaseAddUMagma_and_choice_SubChoice [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_ChoiceBaseAddUMagma_and_eqtype_SubEquality [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.Exports.join_Algebra_SubBaseAddUMagma_between_Algebra_ChoiceBaseAddUMagma_and_eqtype_SubType [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.pack_ [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.SubBaseAddUMagma.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubAddUMagma.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubAddUMagma.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubNmodule.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubNmodule.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubZmodule.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.SubChoice_isSubZmodule.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_AddSemigroup_and_Algebra_SubAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_AddSemigroup_and_Algebra_SubBaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_AddSemigroup_and_choice_SubChoice [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_AddSemigroup_and_eqtype_SubEquality [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_AddSemigroup_and_eqtype_SubType [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_Nmodule_and_Algebra_SubAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_Nmodule_and_Algebra_SubBaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_Nmodule_and_choice_SubChoice [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_Nmodule_and_eqtype_SubEquality [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.Exports.join_Algebra_SubNmodule_between_Algebra_Nmodule_and_eqtype_SubType [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.pack_ [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule_isSubZmodule.phant_axioms [def, in mathcomp.boot.nmodule]
Algebra.SubNmodule_isSubZmodule.phant_Build [def, in mathcomp.boot.nmodule]
Algebra.subr_closed [def, in mathcomp.boot.nmodule]
Algebra.subrK [def, in mathcomp.boot.nmodule]
Algebra.subrr [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_Algebra_BaseZmodule_and_Algebra_SubAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_Algebra_BaseZmodule_and_Algebra_SubBaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_Algebra_BaseZmodule_and_Algebra_SubNmodule [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_Algebra_BaseZmodule_and_choice_SubChoice [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_Algebra_BaseZmodule_and_eqtype_SubEquality [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_Algebra_BaseZmodule_and_eqtype_SubType [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_Algebra_SubAddUMagma_and_Algebra_Zmodule [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_Algebra_SubBaseAddUMagma_and_Algebra_Zmodule [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_Algebra_SubNmodule_and_Algebra_Zmodule [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_choice_SubChoice_and_Algebra_Zmodule [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_eqtype_SubEquality_and_Algebra_Zmodule [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.Exports.join_Algebra_SubZmodule_between_eqtype_SubType_and_Algebra_Zmodule [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.pack_ [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.SubZmodule.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.to_fmultiplicative [def, in mathcomp.boot.nmodule]
Algebra.to_multiplicative [def, in mathcomp.boot.nmodule]
Algebra.to_pmultiplicative [def, in mathcomp.boot.nmodule]
Algebra.zero [def, in mathcomp.boot.nmodule]
Algebra.zmod_closed [def, in mathcomp.boot.nmodule]
Algebra.zmod_morphism [def, in mathcomp.boot.nmodule]
Algebra.ZmodClosed.Exports.join_Algebra_ZmodClosed_between_Algebra_AddClosed_and_Algebra_OppClosed [def, in mathcomp.boot.nmodule]
Algebra.ZmodClosed.pack_ [def, in mathcomp.boot.nmodule]
Algebra.ZmodClosed.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.ZmodClosed.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.Exports.join_Algebra_Zmodule_between_Algebra_AddMagma_and_Algebra_BaseZmodule [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.Exports.join_Algebra_Zmodule_between_Algebra_AddSemigroup_and_Algebra_BaseZmodule [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.Exports.join_Algebra_Zmodule_between_Algebra_AddUMagma_and_Algebra_BaseZmodule [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.Exports.join_Algebra_Zmodule_between_Algebra_BaseZmodule_and_Algebra_ChoiceBaseAddMagma [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.Exports.join_Algebra_Zmodule_between_Algebra_BaseZmodule_and_Algebra_ChoiceBaseAddUMagma [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.Exports.join_Algebra_Zmodule_between_Algebra_BaseZmodule_and_Algebra_Nmodule [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.Exports.join_Algebra_Zmodule_between_Algebra_BaseZmodule_and_choice_Choice [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.Exports.join_Algebra_Zmodule_between_Algebra_BaseZmodule_and_eqtype_Equality [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.pack_ [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.phant_clone [def, in mathcomp.boot.nmodule]
Algebra.Zmodule.phant_on_ [def, in mathcomp.boot.nmodule]
Algebra_isFalgebra.phant_axioms [def, in mathcomp.field.falgebra]
Algebra_isFalgebra.phant_Build [def, in mathcomp.field.falgebra]
algebraicOver [def, in mathcomp.algebra.mxpoly]
Algebraics.divisor [def, in mathcomp.field.algC]
Algebraics.Exports.CdivE [def, in mathcomp.field.algC]
Algebraics.Exports.Crat [def, in mathcomp.field.algC]
Algebraics.Exports.dvdC [def, in mathcomp.field.algC]
Algebraics.Exports.eqCmod [def, in mathcomp.field.algC]
Algebraics.Exports.getCrat [def, in mathcomp.field.algC]
Algebraics.Exports.minCpoly [def, in mathcomp.field.algC]
Algebraics.Implementation.add [def, in mathcomp.field.algC]
Algebraics.Implementation.conj [def, in mathcomp.field.algC]
Algebraics.Implementation.conj_is_additive [def, in mathcomp.field.algC]
Algebraics.Implementation.conj_is_multiplicative [def, in mathcomp.field.algC]
Algebraics.Implementation.conj_is_semi_additive [def, in mathcomp.field.algC]
Algebraics.Implementation.conjL [def, in mathcomp.field.algC]
Algebraics.Implementation.conjMixin [def, in mathcomp.field.algC]
Algebraics.Implementation.CtoL [def, in mathcomp.field.algC]
Algebraics.Implementation.CtoL_is_additive [def, in mathcomp.field.algC]
Algebraics.Implementation.CtoL_is_multiplicative [def, in mathcomp.field.algC]
Algebraics.Implementation.eq_root [def, in mathcomp.field.algC]
Algebraics.Implementation.eq_root_equiv [def, in mathcomp.field.algC]
Algebraics.Implementation.inv [def, in mathcomp.field.algC]
Algebraics.Implementation.isCountable [def, in mathcomp.field.algC]
Algebraics.Implementation.L [def, in mathcomp.field.algC]
Algebraics.Implementation.L' [def, in mathcomp.field.algC]
Algebraics.Implementation.LtoC [def, in mathcomp.field.algC]
Algebraics.Implementation.mul [def, in mathcomp.field.algC]
Algebraics.Implementation.one [def, in mathcomp.field.algC]
Algebraics.Implementation.opp [def, in mathcomp.field.algC]
Algebraics.Implementation.QtoL [def, in mathcomp.field.algC]
Algebraics.Implementation.rootQtoL [def, in mathcomp.field.algC]
Algebraics.Implementation.type [def, in mathcomp.field.algC]
Algebraics.Implementation.zero [def, in mathcomp.field.algC]
Algebraics.Internals.algC_divisor [def, in mathcomp.field.algC]
Algebraics.Internals.int_divisor [def, in mathcomp.field.algC]
Algebraics.Internals.nat_divisor [def, in mathcomp.field.algC]
algid [def, in mathcomp.field.falgebra]
algR_archiFieldMixin [def, in mathcomp.field.algC]
algR_norm [def, in mathcomp.field.algC]
algR_pfactor [def, in mathcomp.field.algC]
algR_rcfMixin [def, in mathcomp.field.algC]
algRval_is_additive [def, in mathcomp.field.algC]
algRval_is_multiplicative [def, in mathcomp.field.algC]
all [def, in mathcomp.boot.seq]
all2 [def, in mathcomp.boot.seq]
all_iff [def, in mathcomp.boot.seq]
allpairs [def, in mathcomp.boot.seq]
allpairs_bseq [def, in mathcomp.boot.tuple]
allpairs_dep [def, in mathcomp.boot.seq]
allpairs_tuple [def, in mathcomp.boot.tuple]
allrel [def, in mathcomp.boot.seq]
Alt [def, in mathcomp.solvable.alt]
Alt_group [def, in mathcomp.solvable.alt]
amove [def, in mathcomp.finite_group.action]
amull [def, in mathcomp.field.falgebra]
amulr [def, in mathcomp.field.falgebra]
amulr_is_multiplicative [def, in mathcomp.field.falgebra]
and3proj1 [def, in mathcomp.boot.ssrbool]
and3proj2 [def, in mathcomp.boot.ssrbool]
and3proj3 [def, in mathcomp.boot.ssrbool]
and4proj1 [def, in mathcomp.boot.ssrbool]
and4proj2 [def, in mathcomp.boot.ssrbool]
and4proj3 [def, in mathcomp.boot.ssrbool]
and4proj4 [def, in mathcomp.boot.ssrbool]
and5proj1 [def, in mathcomp.boot.ssrbool]
and5proj2 [def, in mathcomp.boot.ssrbool]
and5proj3 [def, in mathcomp.boot.ssrbool]
and5proj4 [def, in mathcomp.boot.ssrbool]
and5proj5 [def, in mathcomp.boot.ssrbool]
annihilator_mx [def, in mathcomp.group_representation.mxrepresentation]
aperm [def, in mathcomp.finite_group.perm]
app_fdelta [def, in mathcomp.boot.eqtype]
applybig [def, in mathcomp.boot.bigop]
applyr_head [def, in mathcomp.algebra.sesquilinear]
arc [def, in mathcomp.boot.path]
arg_max [def, in mathcomp.boot.fintype]
arg_min [def, in mathcomp.boot.fintype]
asimple [def, in mathcomp.solvable.jordanholder]
aspace1 [def, in mathcomp.field.falgebra]
aspace_cap [def, in mathcomp.field.falgebra]
aspacef [def, in mathcomp.field.falgebra]
aspaceOver [def, in mathcomp.field.fieldext]
astab [def, in mathcomp.finite_group.action]
astab_group [def, in mathcomp.finite_group.action]
astabs [def, in mathcomp.finite_group.action]
astabs_group [def, in mathcomp.finite_group.action]
atrans [def, in mathcomp.finite_group.action]
aut [def, in mathcomp.finite_group.automorphism]
Aut [def, in mathcomp.finite_group.automorphism]
aut_action [def, in mathcomp.finite_group.action]
Aut_group [def, in mathcomp.finite_group.automorphism]
aut_groupAction [def, in mathcomp.finite_group.action]
aut_Iirr [def, in mathcomp.group_representation.character]
Aut_in [def, in mathcomp.finite_group.action]
Aut_isom [def, in mathcomp.finite_group.automorphism]
Aut_isom_morphism [def, in mathcomp.finite_group.automorphism]
autact [def, in mathcomp.finite_group.action]
autm [def, in mathcomp.finite_group.automorphism]
autm_morphism [def, in mathcomp.finite_group.automorphism]