Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (14626 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (165 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (112 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7292 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (250 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (390 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (84 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3144 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (126 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2221 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (53 entries)

G

gacent [definition, in action]
gacentC [lemma, in action]
gacentD1 [lemma, in action]
gacentE [lemma, in action]
gacentEsd [lemma, in gproduct]
gacentIdom [lemma, in action]
gacentIim [lemma, in action]
gacentJ [lemma, in action]
gacentM [lemma, in action]
gacentQ [lemma, in action]
gacentS [lemma, in action]
gacentU [lemma, in action]
gacentY [lemma, in action]
gacent_repr [lemma, in mxabelem]
gacent_ract [lemma, in action]
gacent_gen [lemma, in action]
gacent_comp [lemma, in action]
gacent_cycle [lemma, in action]
gacent_mod [lemma, in action]
gacent_actby [lemma, in action]
gacent_group [definition, in action]
gacent1 [lemma, in action]
gacent1E [lemma, in action]
gact [projection, in action]
gactJ [lemma, in action]
gactM [lemma, in action]
gactR [lemma, in action]
gactsI [lemma, in jordanholder]
gactsM [lemma, in jordanholder]
gactsP [lemma, in jordanholder]
gacts_range [lemma, in action]
gacts_char [lemma, in action]
gactV [lemma, in action]
gactX [lemma, in action]
gact_stable [lemma, in action]
gact_range [definition, in action]
gact_out [lemma, in action]
gact1 [lemma, in action]
Gaschutz [section, in finmodule]
Gaschutz_transitive [lemma, in finmodule]
Gaschutz_split [lemma, in finmodule]
Gaschutz.abelH [variable, in finmodule]
Gaschutz.coHiPG [variable, in finmodule]
Gaschutz.G [variable, in finmodule]
Gaschutz.gT [variable, in finmodule]
Gaschutz.H [variable, in finmodule]
Gaschutz.nsHG [variable, in finmodule]
Gaschutz.P [variable, in finmodule]
Gaschutz.sHP [variable, in finmodule]
Gaschutz.sPG [variable, in finmodule]
gastabsP [lemma, in jordanholder]
gauss [lemma, in div]
gaussE [abbreviation, in mxalgebra]
gaussian_elimination_map [lemma, in mxalgebra]
gaussian_elimination [definition, in mxalgebra]
gauss_gcdl [lemma, in div]
gauss_inv [lemma, in div]
gauss_gcdr [lemma, in div]
gcdn [definition, in div]
gcdnA [lemma, in div]
gcdnAC [lemma, in div]
gcdnC [lemma, in div]
gcdnCA [lemma, in div]
gcdnE [lemma, in div]
gcdnn [lemma, in div]
gcdn_addr [lemma, in div]
gcdn_mull [lemma, in div]
gcdn_addl [lemma, in div]
gcdn_addl_mul [lemma, in div]
gcdn_mul2l [lemma, in div]
gcdn_mulr [lemma, in div]
gcdn_exp [lemma, in div]
gcdn_modr [lemma, in div]
gcdn_gt0 [lemma, in div]
gcdn_addoid [definition, in bigop]
gcdn_comoid [definition, in bigop]
gcdn_monoid [definition, in bigop]
gcdn_modl [lemma, in div]
gcdn_def [lemma, in div]
gcdn_rec [definition, in div]
gcdn_divnC [lemma, in div]
gcdn0 [lemma, in div]
gcdn1 [lemma, in div]
gcdp [definition, in poly]
gcdpC [lemma, in poly]
gcdpE [lemma, in poly]
gcdpp [lemma, in poly]
gcdp_map [lemma, in poly]
gcdp0 [lemma, in poly]
gcd0n [lemma, in div]
gcd0p [lemma, in poly]
gcd1n [lemma, in div]
Gcl [abbreviation, in fingroup]
gcore [definition, in fingroup]
gcore_sub [lemma, in fingroup]
gcore_group [definition, in fingroup]
gcore_max [lemma, in fingroup]
gcore_norm [lemma, in fingroup]
gcore_normal [lemma, in fingroup]
Gcycg [definition, in finmodule]
genD [lemma, in fingroup]
genDU [lemma, in fingroup]
genD1 [lemma, in fingroup]
genD1id [lemma, in fingroup]
GeneralExponentPextraspecialTheory [section, in extraspecial]
GeneralExponentPextraspecialTheory.p [variable, in extraspecial]
generated [definition, in fingroup]
GeneratedGroup [section, in fingroup]
GeneratedGroup.gT [variable, in fingroup]
generatedP [lemma, in fingroup]
generated_group [definition, in fingroup]
generator [definition, in cyclic]
generators_quaternion [lemma, in extremal]
generators_semidihedral [lemma, in extremal]
generators_modular_group [lemma, in extremal]
generators_2dihedral [lemma, in extremal]
generator_cycle [lemma, in cyclic]
generator_order [lemma, in cyclic]
generator_coprime [lemma, in cyclic]
genGid [lemma, in fingroup]
genGidG [lemma, in fingroup]
genJ [lemma, in fingroup]
genmx [definition, in mxalgebra]
genmxE [lemma, in mxalgebra]
genmxP [lemma, in mxalgebra]
genmx_witness [definition, in mxalgebra]
genmx_def [definition, in mxalgebra]
genmx_key [lemma, in mxalgebra]
genmx_id [lemma, in mxalgebra]
genmx_adds [lemma, in mxalgebra]
genmx_component [lemma, in mxrepresentation]
genmx_sums [lemma, in mxalgebra]
genmx_bigcap [lemma, in mxalgebra]
genmx_witnessP [definition, in mxalgebra]
genmx_muls [lemma, in mxalgebra]
genmx_Socle [lemma, in mxrepresentation]
genmx_diff [lemma, in mxalgebra]
genmx_cap [lemma, in mxalgebra]
genmx0 [lemma, in mxalgebra]
genmx1 [lemma, in mxalgebra]
genM_join [lemma, in fingroup]
genS [lemma, in fingroup]
genV [lemma, in fingroup]
gen_expgs [lemma, in fingroup]
gen_rank [definition, in abelian]
gen_prodgP [lemma, in fingroup]
gen_subG [lemma, in fingroup]
gen_set_id [lemma, in fingroup]
gen0 [lemma, in fingroup]
geq [definition, in ssrnat]
GeqNotLtn [constructor, in ssrnat]
geq_leqif [lemma, in ssrnat]
gFchar [lemma, in gfunctor]
gFcompS [lemma, in gfunctor]
gFcomp_closed [lemma, in gfunctor]
gFcomp_cont [lemma, in gfunctor]
gFcomp_mgFun [definition, in gfunctor]
gFcomp_gFun [definition, in gfunctor]
gFcomp_igFun [definition, in gfunctor]
gFcont [lemma, in gfunctor]
gFgroup [definition, in gfunctor]
gFgroupset [lemma, in gfunctor]
gFhereditary [lemma, in gfunctor]
gFid [lemma, in gfunctor]
gFisog [lemma, in gfunctor]
gFisom [lemma, in gfunctor]
gFiso_cont [lemma, in gfunctor]
gFmod_hereditary [lemma, in gfunctor]
gFmod_cont [lemma, in gfunctor]
gFmod_closed [lemma, in gfunctor]
gFmod_pgFun [definition, in gfunctor]
gFmod_gFun [definition, in gfunctor]
gFmod_igFun [definition, in gfunctor]
gFmod_group [definition, in gfunctor]
gFnorm [lemma, in gfunctor]
gFnormal [lemma, in gfunctor]
gFsub [lemma, in gfunctor]
GFunctor [module, in gfunctor]
gfunctor [library]
GFunctorExamples [section, in gfunctor]
gFunctorI [lemma, in gfunctor]
gFunctorS [lemma, in gfunctor]
GFunctor.apply [projection, in gfunctor]
GFunctor.ClassDefinitions [section, in gfunctor]
GFunctor.clone [definition, in gfunctor]
GFunctor.clone_mono [definition, in gfunctor]
GFunctor.clone_pmap [definition, in gfunctor]
GFunctor.clone_iso [definition, in gfunctor]
GFunctor.closed [definition, in gfunctor]
GFunctor.comp_head [definition, in gfunctor]
GFunctor.continuous [definition, in gfunctor]
GFunctor.continuous_is_iso_continuous [lemma, in gfunctor]
GFunctor.Definitions [section, in gfunctor]
GFunctor.Definitions.F [variable, in gfunctor]
GFunctor.Definitions.F1 [variable, in gfunctor]
GFunctor.Definitions.F2 [variable, in gfunctor]
GFunctor.Definitions.k [variable, in gfunctor]
GFunctor.group_valued [definition, in gfunctor]
GFunctor.hereditary [definition, in gfunctor]
GFunctor.IsoMap [constructor, in gfunctor]
GFunctor.iso_of_map [projection, in gfunctor]
GFunctor.iso_continuous [definition, in gfunctor]
GFunctor.iso_map [record, in gfunctor]
GFunctor.Map [constructor, in gfunctor]
GFunctor.map [record, in gfunctor]
GFunctor.map_of_mono [projection, in gfunctor]
GFunctor.map_of_pmap [projection, in gfunctor]
GFunctor.modulo [definition, in gfunctor]
GFunctor.MonoMap [constructor, in gfunctor]
GFunctor.monotonic [definition, in gfunctor]
GFunctor.mono_map [record, in gfunctor]
GFunctor.object_map [definition, in gfunctor]
GFunctor.pack_iso [definition, in gfunctor]
GFunctor.pcontinuous [definition, in gfunctor]
GFunctor.pcontinuous_is_continuous [lemma, in gfunctor]
GFunctor.pcontinuous_is_hereditary [lemma, in gfunctor]
GFunctor.pmap [record, in gfunctor]
GFunctor.Pmap [constructor, in gfunctor]
gFunc_id [definition, in gfunctor]
gH [abbreviation, in gproduct]
gH [definition, in center]
gK [definition, in center]
gK [abbreviation, in gproduct]
GLgroup [definition, in matrix]
GLgroup_group [definition, in matrix]
GLmx_faithful [lemma, in mxabelem]
GLrepr [definition, in mxabelem]
GLtype [definition, in matrix]
GLval [definition, in matrix]
GL_eqMixin [definition, in matrix]
GL_MxE [lemma, in matrix]
GL_unit.n [variable, in matrix]
GL_1E [lemma, in matrix]
GL_det [lemma, in matrix]
GL_VE [lemma, in matrix]
GL_ME [lemma, in matrix]
GL_unit [lemma, in matrix]
GL_unit.R [variable, in matrix]
GL_finGroupType [definition, in matrix]
GL_baseFinGroupType [definition, in matrix]
GL_subFinType [definition, in matrix]
GL_finType [definition, in matrix]
GL_subCountType [definition, in matrix]
GL_countType [definition, in matrix]
GL_choiceType [definition, in matrix]
GL_eqType [definition, in matrix]
GL_subType [definition, in matrix]
GL_VxE [lemma, in matrix]
GL_unitmx [lemma, in matrix]
GL_mx_repr [lemma, in mxabelem]
GL_unit [section, in matrix]
gnorm [definition, in fingroup]
gof [abbreviation, in morphism]
gproduct [library]
grank_min [lemma, in abelian]
grank_abelian [lemma, in abelian]
grank_witness [lemma, in abelian]
GRing [module, in ssralg]
gring_valK [lemma, in mxrepresentation]
gring_rowK [lemma, in mxrepresentation]
gring_row_mul [lemma, in mxrepresentation]
gring_op_mx [lemma, in mxrepresentation]
gring_op [definition, in mxrepresentation]
gring_op1 [lemma, in mxrepresentation]
gring_opM [lemma, in mxrepresentation]
gring_index [definition, in mxrepresentation]
gring_op_linear [definition, in mxrepresentation]
gring_mx_linear [definition, in mxrepresentation]
gring_proj_linear [definition, in mxrepresentation]
gring_row_linear [definition, in mxrepresentation]
gring_mxP [lemma, in mxrepresentation]
gring_free [lemma, in mxrepresentation]
gring_indexK [lemma, in mxrepresentation]
gring_opG [lemma, in mxrepresentation]
gring_mx [definition, in mxrepresentation]
gring_mxK [lemma, in mxrepresentation]
gring_mxA [lemma, in mxrepresentation]
gring_op_id [lemma, in mxrepresentation]
gring_row [definition, in mxrepresentation]
gring_mxJ [lemma, in mxrepresentation]
gring_opJ [lemma, in mxrepresentation]
gring_proj [definition, in mxrepresentation]
gring_projE [lemma, in mxrepresentation]
gring_opE [lemma, in mxrepresentation]
GRing.add [definition, in ssralg]
GRing.Add [constructor, in ssralg]
GRing.addIr [lemma, in ssralg]
GRing.AdditiveTheory [section, in ssralg]
GRing.AdditiveTheory.AddFun [section, in ssralg]
GRing.AdditiveTheory.AddFun.f [variable, in ssralg]
GRing.AdditiveTheory.AddFun.g [variable, in ssralg]
GRing.AdditiveTheory.AddFun.h [variable, in ssralg]
GRing.AdditiveTheory.AddFun.U [variable, in ssralg]
GRing.AdditiveTheory.AddFun.V [variable, in ssralg]
GRing.AdditiveTheory.AddFun.W [variable, in ssralg]
GRing.AdditiveTheory.MulFun [section, in ssralg]
GRing.AdditiveTheory.MulFun.a [variable, in ssralg]
GRing.AdditiveTheory.MulFun.f [variable, in ssralg]
GRing.AdditiveTheory.MulFun.R [variable, in ssralg]
GRing.AdditiveTheory.MulFun.U [variable, in ssralg]
GRing.AdditiveTheory.Properties [section, in ssralg]
GRing.AdditiveTheory.Properties.f [variable, in ssralg]
GRing.AdditiveTheory.Properties.U [variable, in ssralg]
GRing.AdditiveTheory.Properties.V [variable, in ssralg]
GRing.AdditiveTheory.ScaleFun [section, in ssralg]
GRing.AdditiveTheory.ScaleFun.a [variable, in ssralg]
GRing.AdditiveTheory.ScaleFun.f [variable, in ssralg]
GRing.AdditiveTheory.ScaleFun.R [variable, in ssralg]
GRing.AdditiveTheory.ScaleFun.U [variable, in ssralg]
GRing.AdditiveTheory.ScaleFun.V [variable, in ssralg]
GRing.Additive.apply [projection, in ssralg]
GRing.Additive.axiom [definition, in ssralg]
GRing.Additive.class [definition, in ssralg]
GRing.Additive.ClassDef [section, in ssralg]
GRing.Additive.ClassDef.cF [variable, in ssralg]
GRing.Additive.ClassDef.f [variable, in ssralg]
GRing.Additive.ClassDef.g [variable, in ssralg]
GRing.Additive.ClassDef.phUV [variable, in ssralg]
GRing.Additive.ClassDef.U [variable, in ssralg]
GRing.Additive.ClassDef.V [variable, in ssralg]
GRing.Additive.clone [definition, in ssralg]
GRing.Additive.Exports.additive [abbreviation, in ssralg]
GRing.Additive.Exports.Additive [abbreviation, in ssralg]
GRing.Additive.map [record, in ssralg]
GRing.Additive.Pack [constructor, in ssralg]
GRing.addKr [lemma, in ssralg]
GRing.addNKr [lemma, in ssralg]
GRing.addNr [lemma, in ssralg]
GRing.addoid [definition, in ssralg]
GRing.addrA [lemma, in ssralg]
GRing.addrAC [lemma, in ssralg]
GRing.addrC [lemma, in ssralg]
GRing.addrCA [lemma, in ssralg]
GRing.addrI [lemma, in ssralg]
GRing.addrK [lemma, in ssralg]
GRing.addrN [lemma, in ssralg]
GRing.addrNK [lemma, in ssralg]
GRing.addr_eq0 [lemma, in ssralg]
GRing.addr0 [lemma, in ssralg]
GRing.add_fun_linear [definition, in ssralg]
GRing.add_fun_additive [definition, in ssralg]
GRing.add_comoid [definition, in ssralg]
GRing.add_monoid [definition, in ssralg]
GRing.add_fun_is_scalable [lemma, in ssralg]
GRing.add_fun_is_additive [lemma, in ssralg]
GRing.add_fun_head [definition, in ssralg]
GRing.add0r [lemma, in ssralg]
GRing.AlgebraTheory [section, in ssralg]
GRing.AlgebraTheory.A [variable, in ssralg]
GRing.AlgebraTheory.a [variable, in ssralg]
GRing.AlgebraTheory.f [variable, in ssralg]
GRing.AlgebraTheory.R [variable, in ssralg]
GRing.AlgebraTheory.U [variable, in ssralg]
GRing.Algebra.axiom [definition, in ssralg]
GRing.Algebra.base [projection, in ssralg]
GRing.Algebra.choiceType [definition, in ssralg]
GRing.Algebra.Class [constructor, in ssralg]
GRing.Algebra.class [definition, in ssralg]
GRing.Algebra.ClassDef [section, in ssralg]
GRing.Algebra.ClassDef.cT [variable, in ssralg]
GRing.Algebra.ClassDef.phR [variable, in ssralg]
GRing.Algebra.ClassDef.R [variable, in ssralg]
GRing.Algebra.ClassDef.T [variable, in ssralg]
GRing.Algebra.class_of [record, in ssralg]
GRing.Algebra.clone [definition, in ssralg]
GRing.Algebra.comm_axiom [lemma, in ssralg]
GRing.Algebra.eqType [definition, in ssralg]
GRing.Algebra.Exports.AlgType [abbreviation, in ssralg]
GRing.Algebra.Exports.algType [abbreviation, in ssralg]
GRing.Algebra.Exports.CommAlgType [abbreviation, in ssralg]
GRing.Algebra.lalgType [definition, in ssralg]
GRing.Algebra.lmodType [definition, in ssralg]
GRing.Algebra.Mixin [section, in ssralg]
GRing.Algebra.mixin [projection, in ssralg]
GRing.Algebra.Mixin.A [variable, in ssralg]
GRing.Algebra.Mixin.R [variable, in ssralg]
GRing.Algebra.Pack [constructor, in ssralg]
GRing.Algebra.pack [definition, in ssralg]
GRing.Algebra.ringType [definition, in ssralg]
GRing.Algebra.sort [projection, in ssralg]
GRing.Algebra.type [record, in ssralg]
GRing.Algebra.zmodType [definition, in ssralg]
GRing.And [constructor, in ssralg]
GRing.and_dnfP [lemma, in ssralg]
GRing.and_dnf [definition, in ssralg]
GRing.bij_lrmorphism [lemma, in ssralg]
GRing.bij_linear [lemma, in ssralg]
GRing.bij_rmorphism [lemma, in ssralg]
GRing.bij_additive [lemma, in ssralg]
GRing.bin_lt_charf_0 [lemma, in ssralg]
GRing.Bool [constructor, in ssralg]
GRing.can2_lrmorphism [lemma, in ssralg]
GRing.can2_additive [lemma, in ssralg]
GRing.can2_rmorphism [lemma, in ssralg]
GRing.can2_linear [lemma, in ssralg]
GRing.cat_dnfP [lemma, in ssralg]
GRing.char [definition, in ssralg]
GRing.charf_prime [lemma, in ssralg]
GRing.charf_eq [lemma, in ssralg]
GRing.charf'_nat [lemma, in ssralg]
GRing.charf0 [lemma, in ssralg]
GRing.charf0P [lemma, in ssralg]
GRing.char0_natf_div [lemma, in ssralg]
GRing.ClosedFieldTheory [section, in ssralg]
GRing.ClosedFieldTheory.F [variable, in ssralg]
GRing.ClosedField.axiom [definition, in ssralg]
GRing.ClosedField.base [projection, in ssralg]
GRing.ClosedField.choiceType [definition, in ssralg]
GRing.ClosedField.Class [constructor, in ssralg]
GRing.ClosedField.class [definition, in ssralg]
GRing.ClosedField.ClassDef [section, in ssralg]
GRing.ClosedField.ClassDef.cT [variable, in ssralg]
GRing.ClosedField.ClassDef.T [variable, in ssralg]
GRing.ClosedField.class_of [record, in ssralg]
GRing.ClosedField.clone [definition, in ssralg]
GRing.ClosedField.comRingType [definition, in ssralg]
GRing.ClosedField.comUnitRingType [definition, in ssralg]
GRing.ClosedField.decFieldType [definition, in ssralg]
GRing.ClosedField.eqType [definition, in ssralg]
GRing.ClosedField.Exports.closedFieldType [abbreviation, in ssralg]
GRing.ClosedField.Exports.ClosedFieldType [abbreviation, in ssralg]
GRing.ClosedField.fieldType [definition, in ssralg]
GRing.ClosedField.idomainType [definition, in ssralg]
GRing.ClosedField.pack [definition, in ssralg]
GRing.ClosedField.Pack [constructor, in ssralg]
GRing.ClosedField.ringType [definition, in ssralg]
GRing.ClosedField.sort [projection, in ssralg]
GRing.ClosedField.type [record, in ssralg]
GRing.ClosedField.unitRingType [definition, in ssralg]
GRing.ClosedField.zmodType [definition, in ssralg]
GRing.comm [definition, in ssralg]
GRing.commrN1 [lemma, in ssralg]
GRing.commr_nat [lemma, in ssralg]
GRing.commr_refl [lemma, in ssralg]
GRing.commr_exp [lemma, in ssralg]
GRing.commr_opp [lemma, in ssralg]
GRing.commr_muln [lemma, in ssralg]
GRing.commr_mul [lemma, in ssralg]
GRing.commr_unit_mul [lemma, in ssralg]
GRing.commr_inv [lemma, in ssralg]
GRing.commr_sign [lemma, in ssralg]
GRing.commr_exp_mull [lemma, in ssralg]
GRing.commr_add [lemma, in ssralg]
GRing.commr_sym [lemma, in ssralg]
GRing.commr0 [lemma, in ssralg]
GRing.commr1 [lemma, in ssralg]
GRing.comp_linear [definition, in ssralg]
GRing.comp_rmorphism [definition, in ssralg]
GRing.comp_additive [definition, in ssralg]
GRing.comp_is_additive [lemma, in ssralg]
GRing.comp_lrmorphism [definition, in ssralg]
GRing.comp_is_multiplicative [definition, in ssralg]
GRing.comp_is_scalable [lemma, in ssralg]
GRing.ComRingTheory [section, in ssralg]
GRing.ComRingTheory.FrobeniusAutomorphism [section, in ssralg]
GRing.ComRingTheory.FrobeniusAutomorphism.charRp [variable, in ssralg]
GRing.ComRingTheory.FrobeniusAutomorphism.p [variable, in ssralg]
GRing.ComRingTheory.R [variable, in ssralg]
GRing.ComRingTheory.ScaleLinear [section, in ssralg]
GRing.ComRingTheory.ScaleLinear.b [variable, in ssralg]
GRing.ComRingTheory.ScaleLinear.f [variable, in ssralg]
GRing.ComRingTheory.ScaleLinear.U [variable, in ssralg]
GRing.ComRingTheory.ScaleLinear.V [variable, in ssralg]
GRing.ComRing.base [projection, in ssralg]
GRing.ComRing.choiceType [definition, in ssralg]
GRing.ComRing.Class [constructor, in ssralg]
GRing.ComRing.class [definition, in ssralg]
GRing.ComRing.ClassDef [section, in ssralg]
GRing.ComRing.ClassDef.cT [variable, in ssralg]
GRing.ComRing.ClassDef.T [variable, in ssralg]
GRing.ComRing.class_of [record, in ssralg]
GRing.ComRing.clone [definition, in ssralg]
GRing.ComRing.eqType [definition, in ssralg]
GRing.ComRing.Exports.ComRingMixin [abbreviation, in ssralg]
GRing.ComRing.Exports.ComRingType [abbreviation, in ssralg]
GRing.ComRing.Exports.comRingType [abbreviation, in ssralg]
GRing.ComRing.Pack [constructor, in ssralg]
GRing.ComRing.pack [definition, in ssralg]
GRing.ComRing.RingMixin [definition, in ssralg]
GRing.ComRing.ringType [definition, in ssralg]
GRing.ComRing.sort [projection, in ssralg]
GRing.ComRing.type [record, in ssralg]
GRing.ComRing.zmodType [definition, in ssralg]
GRing.ComUnitRingTheory [section, in ssralg]
GRing.ComUnitRingTheory.R [variable, in ssralg]
GRing.ComUnitRing.base [projection, in ssralg]
GRing.ComUnitRing.base2 [definition, in ssralg]
GRing.ComUnitRing.choiceType [definition, in ssralg]
GRing.ComUnitRing.class [definition, in ssralg]
GRing.ComUnitRing.Class [constructor, in ssralg]
GRing.ComUnitRing.ClassDef [section, in ssralg]
GRing.ComUnitRing.ClassDef.cT [variable, in ssralg]
GRing.ComUnitRing.ClassDef.T [variable, in ssralg]
GRing.ComUnitRing.class_of [record, in ssralg]
GRing.ComUnitRing.comRingType [definition, in ssralg]
GRing.ComUnitRing.com_unitRingType [definition, in ssralg]
GRing.ComUnitRing.eqType [definition, in ssralg]
GRing.ComUnitRing.Exports.ComUnitRingMixin [abbreviation, in ssralg]
GRing.ComUnitRing.Exports.comUnitRingType [abbreviation, in ssralg]
GRing.ComUnitRing.Mixin [definition, in ssralg]
GRing.ComUnitRing.Mixin [section, in ssralg]
GRing.ComUnitRing.mixin [projection, in ssralg]
GRing.ComUnitRing.Mixin.inv [variable, in ssralg]
GRing.ComUnitRing.Mixin.mulVx [variable, in ssralg]
GRing.ComUnitRing.Mixin.R [variable, in ssralg]
GRing.ComUnitRing.Mixin.unit [variable, in ssralg]
GRing.ComUnitRing.Mixin.unitPl [variable, in ssralg]
GRing.ComUnitRing.mulC_unitP [lemma, in ssralg]
GRing.ComUnitRing.mulC_mulrV [lemma, in ssralg]
GRing.ComUnitRing.pack [definition, in ssralg]
GRing.ComUnitRing.Pack [constructor, in ssralg]
GRing.ComUnitRing.ringType [definition, in ssralg]
GRing.ComUnitRing.sort [projection, in ssralg]
GRing.ComUnitRing.type [record, in ssralg]
GRing.ComUnitRing.unitRingType [definition, in ssralg]
GRing.ComUnitRing.zmodType [definition, in ssralg]
GRing.Const [constructor, in ssralg]
GRing.converse [definition, in ssralg]
GRing.converse_ringMixin [definition, in ssralg]
GRing.converse_unitRingType [definition, in ssralg]
GRing.converse_ringType [definition, in ssralg]
GRing.converse_zmodType [definition, in ssralg]
GRing.converse_choiceType [definition, in ssralg]
GRing.converse_eqType [definition, in ssralg]
GRing.converse_unitRingMixin [definition, in ssralg]
GRing.DecidableFieldTheory [section, in ssralg]
GRing.DecidableFieldTheory.F [variable, in ssralg]
GRing.DecidableField.axiom [definition, in ssralg]
GRing.DecidableField.base [projection, in ssralg]
GRing.DecidableField.choiceType [definition, in ssralg]
GRing.DecidableField.Class [constructor, in ssralg]
GRing.DecidableField.class [definition, in ssralg]
GRing.DecidableField.ClassDef [section, in ssralg]
GRing.DecidableField.ClassDef.cT [variable, in ssralg]
GRing.DecidableField.ClassDef.T [variable, in ssralg]
GRing.DecidableField.class_of [record, in ssralg]
GRing.DecidableField.clone [definition, in ssralg]
GRing.DecidableField.comRingType [definition, in ssralg]
GRing.DecidableField.comUnitRingType [definition, in ssralg]
GRing.DecidableField.eqType [definition, in ssralg]
GRing.DecidableField.Exports.DecFieldMixin [abbreviation, in ssralg]
GRing.DecidableField.Exports.DecFieldType [abbreviation, in ssralg]
GRing.DecidableField.Exports.decFieldType [abbreviation, in ssralg]
GRing.DecidableField.fieldType [definition, in ssralg]
GRing.DecidableField.idomainType [definition, in ssralg]
GRing.DecidableField.Mixin [constructor, in ssralg]
GRing.DecidableField.mixin [projection, in ssralg]
GRing.DecidableField.mixin_of [record, in ssralg]
GRing.DecidableField.Pack [constructor, in ssralg]
GRing.DecidableField.pack [definition, in ssralg]
GRing.DecidableField.ringType [definition, in ssralg]
GRing.DecidableField.sat [projection, in ssralg]
GRing.DecidableField.satP [projection, in ssralg]
GRing.DecidableField.sort [projection, in ssralg]
GRing.DecidableField.type [record, in ssralg]
GRing.DecidableField.unitRingType [definition, in ssralg]
GRing.DecidableField.zmodType [definition, in ssralg]
GRing.divff [lemma, in ssralg]
GRing.divfK [definition, in ssralg]
GRing.divrK [definition, in ssralg]
GRing.divrr [lemma, in ssralg]
GRing.divr1 [lemma, in ssralg]
GRing.div1r [lemma, in ssralg]
GRing.dnf_to_form [definition, in ssralg]
GRing.dnf_to_form_qf [lemma, in ssralg]
GRing.dnf_rterm [definition, in ssralg]
GRing.dnf_to_rform [lemma, in ssralg]
GRing.dvdn_charf [lemma, in ssralg]
GRing.elim_aux [definition, in ssralg]
GRing.eqr_opp [lemma, in ssralg]
GRing.eqr_oppC [lemma, in ssralg]
GRing.Equal [constructor, in ssralg]
GRing.eq_eval [lemma, in ssralg]
GRing.eq_sat [lemma, in ssralg]
GRing.eq_sol [lemma, in ssralg]
GRing.eq_holds [lemma, in ssralg]
GRing.eq0_rform [definition, in ssralg]
GRing.eval [definition, in ssralg]
GRing.EvalTerm [section, in ssralg]
GRing.EvalTerm.MultiQuant [section, in ssralg]
GRing.EvalTerm.MultiQuant.f [variable, in ssralg]
GRing.EvalTerm.Pick [section, in ssralg]
GRing.EvalTerm.Pick.else_f [variable, in ssralg]
GRing.EvalTerm.Pick.I [variable, in ssralg]
GRing.EvalTerm.Pick.pred_f [variable, in ssralg]
GRing.EvalTerm.Pick.then_f [variable, in ssralg]
GRing.EvalTerm.R [variable, in ssralg]
GRing.eval_Pick [lemma, in ssralg]
GRing.eval_tsubst [lemma, in ssralg]
GRing.Exists [constructor, in ssralg]
GRing.Exp [constructor, in ssralg]
GRing.exp [definition, in ssralg]
GRing.expfS_eq1 [lemma, in ssralg]
GRing.expf_neq0 [lemma, in ssralg]
GRing.expf_eq0 [lemma, in ssralg]
GRing.exprN [lemma, in ssralg]
GRing.exprn_addr [lemma, in ssralg]
GRing.exprn_subl_comm [lemma, in ssralg]
GRing.exprn_mod [lemma, in ssralg]
GRing.exprn_subl [lemma, in ssralg]
GRing.exprn_addl_comm [lemma, in ssralg]
GRing.exprn_addl [lemma, in ssralg]
GRing.exprn_dvd [lemma, in ssralg]
GRing.exprn_mulr [lemma, in ssralg]
GRing.exprn_mull [lemma, in ssralg]
GRing.exprn_add1 [lemma, in ssralg]
GRing.exprn_mulnl [lemma, in ssralg]
GRing.exprS [lemma, in ssralg]
GRing.exprSr [lemma, in ssralg]
GRing.expr_inv [lemma, in ssralg]
GRing.expr0 [lemma, in ssralg]
GRing.expr1 [lemma, in ssralg]
GRing.expr2 [lemma, in ssralg]
GRing.exp1rn [lemma, in ssralg]
GRing.False [abbreviation, in ssralg]
GRing.fE [abbreviation, in ssralg]
GRing.FieldTheory [section, in ssralg]
GRing.FieldTheory.F [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInj [section, in ssralg]
GRing.FieldTheory.FieldMorphismInj.f [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInj.R [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInv [section, in ssralg]
GRing.FieldTheory.FieldMorphismInv.f [variable, in ssralg]
GRing.FieldTheory.FieldMorphismInv.R [variable, in ssralg]
GRing.FieldTheory.ModuleTheory [section, in ssralg]
GRing.FieldTheory.ModuleTheory.V [variable, in ssralg]
GRing.Field.axiom [definition, in ssralg]
GRing.Field.base [projection, in ssralg]
GRing.Field.choiceType [definition, in ssralg]
GRing.Field.Class [constructor, in ssralg]
GRing.Field.class [definition, in ssralg]
GRing.Field.ClassDef [section, in ssralg]
GRing.Field.ClassDef.cT [variable, in ssralg]
GRing.Field.ClassDef.T [variable, in ssralg]
GRing.Field.class_of [record, in ssralg]
GRing.Field.clone [definition, in ssralg]
GRing.Field.comRingType [definition, in ssralg]
GRing.Field.comUnitRingType [definition, in ssralg]
GRing.Field.eqType [definition, in ssralg]
GRing.Field.Exports.FieldIdomainMixin [abbreviation, in ssralg]
GRing.Field.Exports.FieldMixin [abbreviation, in ssralg]
GRing.Field.Exports.FieldType [abbreviation, in ssralg]
GRing.Field.Exports.fieldType [abbreviation, in ssralg]
GRing.Field.Exports.FieldUnitMixin [abbreviation, in ssralg]
GRing.Field.IdomainMixin [lemma, in ssralg]
GRing.Field.idomainType [definition, in ssralg]
GRing.Field.intro_unit [lemma, in ssralg]
GRing.Field.inv_out [lemma, in ssralg]
GRing.Field.Mixin [lemma, in ssralg]
GRing.Field.Mixins [section, in ssralg]
GRing.Field.Mixins.inv [variable, in ssralg]
GRing.Field.Mixins.inv0 [variable, in ssralg]
GRing.Field.Mixins.mulVx [variable, in ssralg]
GRing.Field.Mixins.R [variable, in ssralg]
GRing.Field.mixin_of [definition, in ssralg]
GRing.Field.pack [definition, in ssralg]
GRing.Field.Pack [constructor, in ssralg]
GRing.Field.ringType [definition, in ssralg]
GRing.Field.sort [projection, in ssralg]
GRing.Field.type [record, in ssralg]
GRing.Field.UnitMixin [definition, in ssralg]
GRing.Field.unitRingType [definition, in ssralg]
GRing.Field.zmodType [definition, in ssralg]
GRing.fmorphV [lemma, in ssralg]
GRing.fmorph_eq0 [lemma, in ssralg]
GRing.fmorph_char [lemma, in ssralg]
GRing.fmorph_inj [lemma, in ssralg]
GRing.fmorph_div [lemma, in ssralg]
GRing.fmorph_unit [lemma, in ssralg]
GRing.foldExistsP [lemma, in ssralg]
GRing.foldForallP [lemma, in ssralg]
GRing.Forall [constructor, in ssralg]
GRing.formula [inductive, in ssralg]
GRing.Frobenius_aut_0 [lemma, in ssralg]
GRing.Frobenius_aut_is_rmorphism [lemma, in ssralg]
GRing.Frobenius_aut_rmorphism [definition, in ssralg]
GRing.Frobenius_aut_additive [definition, in ssralg]
GRing.Frobenius_aut_1 [lemma, in ssralg]
GRing.Frobenius_aut_muln [lemma, in ssralg]
GRing.Frobenius_aut_mul_comm [lemma, in ssralg]
GRing.Frobenius_aut [definition, in ssralg]
GRing.Frobenius_aut_sub_comm [lemma, in ssralg]
GRing.Frobenius_aut_exp [lemma, in ssralg]
GRing.Frobenius_aut_add_comm [lemma, in ssralg]
GRing.Frobenius_aut_nat [lemma, in ssralg]
GRing.Frobenius_autE [lemma, in ssralg]
GRing.Frobenius_aut_opp [lemma, in ssralg]
GRing.fsubst [definition, in ssralg]
GRing.holds [definition, in ssralg]
GRing.holds_fsubst [lemma, in ssralg]
GRing.holds_proj [lemma, in ssralg]
GRing.idfun_is_multiplicative [lemma, in ssralg]
GRing.idfun_is_scalable [lemma, in ssralg]
GRing.idfun_linear [definition, in ssralg]
GRing.idfun_rmorphism [definition, in ssralg]
GRing.idfun_additive [definition, in ssralg]
GRing.idfun_lrmorphism [definition, in ssralg]
GRing.idfun_is_additive [lemma, in ssralg]
GRing.Implies [constructor, in ssralg]
GRing.IntegralDomainTheory [section, in ssralg]
GRing.IntegralDomainTheory.R [variable, in ssralg]
GRing.IntegralDomain.axiom [definition, in ssralg]
GRing.IntegralDomain.base [projection, in ssralg]
GRing.IntegralDomain.choiceType [definition, in ssralg]
GRing.IntegralDomain.class [definition, in ssralg]
GRing.IntegralDomain.Class [constructor, in ssralg]
GRing.IntegralDomain.ClassDef [section, in ssralg]
GRing.IntegralDomain.ClassDef.cT [variable, in ssralg]
GRing.IntegralDomain.ClassDef.T [variable, in ssralg]
GRing.IntegralDomain.class_of [record, in ssralg]
GRing.IntegralDomain.clone [definition, in ssralg]
GRing.IntegralDomain.comRingType [definition, in ssralg]
GRing.IntegralDomain.comUnitRingType [definition, in ssralg]
GRing.IntegralDomain.eqType [definition, in ssralg]
GRing.IntegralDomain.Exports.idomainType [abbreviation, in ssralg]
GRing.IntegralDomain.Exports.IdomainType [abbreviation, in ssralg]
GRing.IntegralDomain.pack [definition, in ssralg]
GRing.IntegralDomain.Pack [constructor, in ssralg]
GRing.IntegralDomain.ringType [definition, in ssralg]
GRing.IntegralDomain.sort [projection, in ssralg]
GRing.IntegralDomain.type [record, in ssralg]
GRing.IntegralDomain.unitRingType [definition, in ssralg]
GRing.IntegralDomain.zmodType [definition, in ssralg]
GRing.Inv [constructor, in ssralg]
GRing.inv [definition, in ssralg]
GRing.invf_mul [lemma, in ssralg]
GRing.invrK [lemma, in ssralg]
GRing.invrN [lemma, in ssralg]
GRing.invr_neq0 [lemma, in ssralg]
GRing.invr_eq0 [lemma, in ssralg]
GRing.invr_mul [lemma, in ssralg]
GRing.invr_inj [lemma, in ssralg]
GRing.invr_out [lemma, in ssralg]
GRing.invr0 [lemma, in ssralg]
GRing.invr1 [lemma, in ssralg]
GRing.in_alg_rmorphism [definition, in ssralg]
GRing.in_alg_additive [definition, in ssralg]
GRing.in_alg_loc [abbreviation, in ssralg]
GRing.in_alg [abbreviation, in ssralg]
GRing.in_alg_is_rmorphism [lemma, in ssralg]
GRing.in_alg_head [definition, in ssralg]
GRing.LalgebraTheory [section, in ssralg]
GRing.LalgebraTheory.A [variable, in ssralg]
GRing.LalgebraTheory.R [variable, in ssralg]
GRing.Lalgebra.axiom [definition, in ssralg]
GRing.Lalgebra.base [projection, in ssralg]
GRing.Lalgebra.base2 [definition, in ssralg]
GRing.Lalgebra.choiceType [definition, in ssralg]
GRing.Lalgebra.class [definition, in ssralg]
GRing.Lalgebra.Class [constructor, in ssralg]
GRing.Lalgebra.ClassDef [section, in ssralg]
GRing.Lalgebra.ClassDef.cT [variable, in ssralg]
GRing.Lalgebra.ClassDef.phR [variable, in ssralg]
GRing.Lalgebra.ClassDef.R [variable, in ssralg]
GRing.Lalgebra.ClassDef.T [variable, in ssralg]
GRing.Lalgebra.class_of [record, in ssralg]
GRing.Lalgebra.clone [definition, in ssralg]
GRing.Lalgebra.eqType [definition, in ssralg]
GRing.Lalgebra.Exports.lalgType [abbreviation, in ssralg]
GRing.Lalgebra.Exports.LalgType [abbreviation, in ssralg]
GRing.Lalgebra.ext [projection, in ssralg]
GRing.Lalgebra.lmodType [definition, in ssralg]
GRing.Lalgebra.lmod_ringType [definition, in ssralg]
GRing.Lalgebra.mixin [projection, in ssralg]
GRing.Lalgebra.Pack [constructor, in ssralg]
GRing.Lalgebra.pack [definition, in ssralg]
GRing.Lalgebra.ringType [definition, in ssralg]
GRing.Lalgebra.sort [projection, in ssralg]
GRing.Lalgebra.type [record, in ssralg]
GRing.Lalgebra.zmodType [definition, in ssralg]
GRing.LiftedRing [section, in ssralg]
GRing.LiftedRing.R [variable, in ssralg]
GRing.LiftedRing.T [variable, in ssralg]
GRing.LiftedScale [section, in ssralg]
GRing.LiftedScale.A [variable, in ssralg]
GRing.LiftedScale.R [variable, in ssralg]
GRing.LiftedScale.U [variable, in ssralg]
GRing.LiftedScale.V [variable, in ssralg]
GRing.LiftedZmod [section, in ssralg]
GRing.LiftedZmod.U [variable, in ssralg]
GRing.LiftedZmod.V [variable, in ssralg]
GRing.linearD [lemma, in ssralg]
GRing.linearMn [lemma, in ssralg]
GRing.linearMNn [lemma, in ssralg]
GRing.linearN [lemma, in ssralg]
GRing.linearP [lemma, in ssralg]
GRing.LinearTheory [section, in ssralg]
GRing.LinearTheory.LinearLalg [section, in ssralg]
GRing.LinearTheory.LinearLalg.A [variable, in ssralg]
GRing.LinearTheory.LinearLalg.a [variable, in ssralg]
GRing.LinearTheory.LinearLalg.f [variable, in ssralg]
GRing.LinearTheory.LinearLalg.U [variable, in ssralg]
GRing.LinearTheory.LinearLmod [section, in ssralg]
GRing.LinearTheory.LinearLmod.f [variable, in ssralg]
GRing.LinearTheory.LinearLmod.g [variable, in ssralg]
GRing.LinearTheory.LinearLmod.h [variable, in ssralg]
GRing.LinearTheory.LinearLmod.U [variable, in ssralg]
GRing.LinearTheory.LinearLmod.V [variable, in ssralg]
GRing.LinearTheory.LinearLmod.W [variable, in ssralg]
GRing.LinearTheory.Properties [section, in ssralg]
GRing.LinearTheory.Properties.f [variable, in ssralg]
GRing.LinearTheory.Properties.U [variable, in ssralg]
GRing.LinearTheory.Properties.V [variable, in ssralg]
GRing.LinearTheory.R [variable, in ssralg]
GRing.linearZ [lemma, in ssralg]
GRing.linear_sub [lemma, in ssralg]
GRing.linear_sum [lemma, in ssralg]
GRing.Linear.additive [definition, in ssralg]
GRing.Linear.apply [projection, in ssralg]
GRing.Linear.axiom [definition, in ssralg]
GRing.Linear.base [projection, in ssralg]
GRing.Linear.Class [constructor, in ssralg]
GRing.Linear.class [definition, in ssralg]
GRing.Linear.ClassDef [section, in ssralg]
GRing.Linear.ClassDef.cF [variable, in ssralg]
GRing.Linear.ClassDef.f [variable, in ssralg]
GRing.Linear.ClassDef.g [variable, in ssralg]
GRing.Linear.ClassDef.phUV [variable, in ssralg]
GRing.Linear.ClassDef.R [variable, in ssralg]
GRing.Linear.ClassDef.U [variable, in ssralg]
GRing.Linear.ClassDef.V [variable, in ssralg]
GRing.Linear.class_of [record, in ssralg]
GRing.Linear.class_of_axiom [lemma, in ssralg]
GRing.Linear.clone [definition, in ssralg]
GRing.Linear.Exports.AddLinear [abbreviation, in ssralg]
GRing.Linear.Exports.linear [abbreviation, in ssralg]
GRing.Linear.Exports.Linear [abbreviation, in ssralg]
GRing.Linear.Exports.lmorphism [abbreviation, in ssralg]
GRing.Linear.Exports.scalable [abbreviation, in ssralg]
GRing.Linear.map [record, in ssralg]
GRing.Linear.mixin [projection, in ssralg]
GRing.Linear.mixin_of [definition, in ssralg]
GRing.Linear.Pack [constructor, in ssralg]
GRing.Linear.pack [definition, in ssralg]
GRing.linear0 [lemma, in ssralg]
GRing.LmoduleTheory [section, in ssralg]
GRing.LmoduleTheory.R [variable, in ssralg]
GRing.LmoduleTheory.V [variable, in ssralg]
GRing.Lmodule.base [projection, in ssralg]
GRing.Lmodule.choiceType [definition, in ssralg]
GRing.Lmodule.class [definition, in ssralg]
GRing.Lmodule.Class [constructor, in ssralg]
GRing.Lmodule.ClassDef [section, in ssralg]
GRing.Lmodule.ClassDef.cT [variable, in ssralg]
GRing.Lmodule.ClassDef.phR [variable, in ssralg]
GRing.Lmodule.ClassDef.R [variable, in ssralg]
GRing.Lmodule.ClassDef.T [variable, in ssralg]
GRing.Lmodule.class_of [record, in ssralg]
GRing.Lmodule.clone [definition, in ssralg]
GRing.Lmodule.eqType [definition, in ssralg]
GRing.Lmodule.Exports.LmodMixin [abbreviation, in ssralg]
GRing.Lmodule.Exports.lmodType [abbreviation, in ssralg]
GRing.Lmodule.Exports.LmodType [abbreviation, in ssralg]
GRing.Lmodule.Mixin [constructor, in ssralg]
GRing.Lmodule.mixin [projection, in ssralg]
GRing.Lmodule.mixin_of [record, in ssralg]
GRing.Lmodule.pack [definition, in ssralg]
GRing.Lmodule.Pack [constructor, in ssralg]
GRing.Lmodule.scale [projection, in ssralg]
GRing.Lmodule.sort [projection, in ssralg]
GRing.Lmodule.type [record, in ssralg]
GRing.Lmodule.zmodType [definition, in ssralg]
GRing.LRMorphismTheory [section, in ssralg]
GRing.LRMorphismTheory.A [variable, in ssralg]
GRing.LRMorphismTheory.B [variable, in ssralg]
GRing.LRMorphismTheory.C [variable, in ssralg]
GRing.LRMorphismTheory.f [variable, in ssralg]
GRing.LRMorphismTheory.R [variable, in ssralg]
GRing.LRMorphism.additive [definition, in ssralg]
GRing.LRMorphism.apply [projection, in ssralg]
GRing.LRMorphism.base [projection, in ssralg]
GRing.LRMorphism.base2 [definition, in ssralg]
GRing.LRMorphism.class [definition, in ssralg]
GRing.LRMorphism.Class [constructor, in ssralg]
GRing.LRMorphism.ClassDef [section, in ssralg]
GRing.LRMorphism.ClassDef.A [variable, in ssralg]
GRing.LRMorphism.ClassDef.B [variable, in ssralg]
GRing.LRMorphism.ClassDef.cF [variable, in ssralg]
GRing.LRMorphism.ClassDef.f [variable, in ssralg]
GRing.LRMorphism.ClassDef.phAB [variable, in ssralg]
GRing.LRMorphism.ClassDef.R [variable, in ssralg]
GRing.LRMorphism.class_of [record, in ssralg]
GRing.LRMorphism.clone [definition, in ssralg]
GRing.LRMorphism.Exports.lrmorphism [abbreviation, in ssralg]
GRing.LRMorphism.Exports.LRMorphism [abbreviation, in ssralg]
GRing.LRMorphism.join_linear [definition, in ssralg]
GRing.LRMorphism.join_rmorphism [definition, in ssralg]
GRing.LRMorphism.linear [definition, in ssralg]
GRing.LRMorphism.map [record, in ssralg]
GRing.LRMorphism.mixin [projection, in ssralg]
GRing.LRMorphism.Pack [constructor, in ssralg]
GRing.LRMorphism.pack [definition, in ssralg]
GRing.LRMorphism.rmorphism [definition, in ssralg]
GRing.mul [definition, in ssralg]
GRing.Mul [constructor, in ssralg]
GRing.mulfI [lemma, in ssralg]
GRing.mulfK [lemma, in ssralg]
GRing.mulfV [definition, in ssralg]
GRing.mulfVK [lemma, in ssralg]
GRing.mulf_eq0 [lemma, in ssralg]
GRing.mulf_neq0 [lemma, in ssralg]
GRing.mulIf [lemma, in ssralg]
GRing.mulIr [lemma, in ssralg]
GRing.mulKf [lemma, in ssralg]
GRing.mulKr [lemma, in ssralg]
GRing.mull_fun_is_additive [lemma, in ssralg]
GRing.mull_fun_linear [definition, in ssralg]
GRing.mull_fun_additive [definition, in ssralg]
GRing.mull_fun_head [definition, in ssralg]
GRing.mull_fun_is_scalable [lemma, in ssralg]
GRing.mulNr [lemma, in ssralg]
GRing.mulNrn [lemma, in ssralg]
GRing.mulN1r [lemma, in ssralg]
GRing.muloid [definition, in ssralg]
GRing.mulrA [lemma, in ssralg]
GRing.mulrAC [lemma, in ssralg]
GRing.mulrb [lemma, in ssralg]
GRing.mulrC [lemma, in ssralg]
GRing.mulrCA [lemma, in ssralg]
GRing.mulrI [lemma, in ssralg]
GRing.mulrK [lemma, in ssralg]
GRing.mulrN [lemma, in ssralg]
GRing.mulrnA [lemma, in ssralg]
GRing.mulrnAC [lemma, in ssralg]
GRing.mulrnAl [lemma, in ssralg]
GRing.mulrnAr [lemma, in ssralg]
GRing.mulrNN [lemma, in ssralg]
GRing.mulrn_subr [lemma, in ssralg]
GRing.mulrn_addr [lemma, in ssralg]
GRing.mulrn_subl [lemma, in ssralg]
GRing.mulrn_addl [lemma, in ssralg]
GRing.mulrN1 [lemma, in ssralg]
GRing.mulrS [lemma, in ssralg]
GRing.mulrSr [lemma, in ssralg]
GRing.mulrV [definition, in ssralg]
GRing.mulrVK [lemma, in ssralg]
GRing.mulr_fun_linear [definition, in ssralg]
GRing.mulr_fun_additive [definition, in ssralg]
GRing.mulr_fun_is_scalable [lemma, in ssralg]
GRing.mulr_fun_head [definition, in ssralg]
GRing.mulr_addl [lemma, in ssralg]
GRing.mulr_fun_is_additive [lemma, in ssralg]
GRing.mulr_addr [lemma, in ssralg]
GRing.mulr_natr [lemma, in ssralg]
GRing.mulr_suml [lemma, in ssralg]
GRing.mulr_subl [lemma, in ssralg]
GRing.mulr_sumr [lemma, in ssralg]
GRing.mulr_subr [lemma, in ssralg]
GRing.mulr_natl [lemma, in ssralg]
GRing.mulr0 [lemma, in ssralg]
GRing.mulr0n [lemma, in ssralg]
GRing.mulr1 [lemma, in ssralg]
GRing.mulr1n [lemma, in ssralg]
GRing.mulr2n [lemma, in ssralg]
GRing.mulVf [lemma, in ssralg]
GRing.mulVKf [lemma, in ssralg]
GRing.mulVKr [lemma, in ssralg]
GRing.mulVr [lemma, in ssralg]
GRing.mul_comoid [definition, in ssralg]
GRing.mul_monoid [definition, in ssralg]
GRing.mul0r [lemma, in ssralg]
GRing.mul0rn [lemma, in ssralg]
GRing.mul1r [lemma, in ssralg]
GRing.NatConst [constructor, in ssralg]
GRing.natf0_char [lemma, in ssralg]
GRing.NatMul [constructor, in ssralg]
GRing.natmul [definition, in ssralg]
GRing.natr_sub [lemma, in ssralg]
GRing.natr_exp [lemma, in ssralg]
GRing.natr_div [lemma, in ssralg]
GRing.natr_add [lemma, in ssralg]
GRing.natr_mul [lemma, in ssralg]
GRing.natr_sum [definition, in ssralg]
GRing.nonzero1r [lemma, in ssralg]
GRing.Not [constructor, in ssralg]
GRing.null_fun_linear [definition, in ssralg]
GRing.null_fun_additive [definition, in ssralg]
GRing.null_fun_is_scalable [lemma, in ssralg]
GRing.null_fun [abbreviation, in ssralg]
GRing.null_fun_head [definition, in ssralg]
GRing.null_fun_is_additive [lemma, in ssralg]
GRing.one [definition, in ssralg]
GRing.oner_eq0 [lemma, in ssralg]
GRing.Opp [constructor, in ssralg]
GRing.opp [definition, in ssralg]
GRing.opprK [lemma, in ssralg]
GRing.oppr_add [lemma, in ssralg]
GRing.oppr_sub [lemma, in ssralg]
GRing.oppr_eq0 [lemma, in ssralg]
GRing.oppr0 [lemma, in ssralg]
GRing.opp_linear [definition, in ssralg]
GRing.opp_additive [definition, in ssralg]
GRing.opp_is_scalable [lemma, in ssralg]
GRing.opp_is_additive [lemma, in ssralg]
GRing.Or [constructor, in ssralg]
GRing.Pick [definition, in ssralg]
GRing.Pick_form_qf [lemma, in ssralg]
GRing.prodf_inv [lemma, in ssralg]
GRing.prodr_exp_r [lemma, in ssralg]
GRing.prodr_exp [lemma, in ssralg]
GRing.prodr_opp [lemma, in ssralg]
GRing.prodr_const [lemma, in ssralg]
GRing.proj [definition, in ssralg]
GRing.proj_sat [definition, in ssralg]
GRing.proj_satP [lemma, in ssralg]
GRing.QEDecidableField [definition, in ssralg]
GRing.QEDecidableFieldMixin [definition, in ssralg]
GRing.QE_theory.F [variable, in ssralg]
GRing.QE_theory [section, in ssralg]
GRing.QE.Axioms [section, in ssralg]
GRing.QE.Axioms.proj [variable, in ssralg]
GRing.QE.Axioms.R [variable, in ssralg]
GRing.QE.base [projection, in ssralg]
GRing.QE.choiceType [definition, in ssralg]
GRing.QE.class [definition, in ssralg]
GRing.QE.Class [constructor, in ssralg]
GRing.QE.ClassDef [section, in ssralg]
GRing.QE.ClassDef.cT [variable, in ssralg]
GRing.QE.ClassDef.T [variable, in ssralg]
GRing.QE.class_of [record, in ssralg]
GRing.QE.clone [definition, in ssralg]
GRing.QE.comRingType [definition, in ssralg]
GRing.QE.comUnitRingType [definition, in ssralg]
GRing.QE.eqType [definition, in ssralg]
GRing.QE.fieldType [definition, in ssralg]
GRing.QE.holds_proj_axiom [definition, in ssralg]
GRing.QE.holds_proj [projection, in ssralg]
GRing.QE.idomainType [definition, in ssralg]
GRing.QE.mixin [projection, in ssralg]
GRing.QE.Mixin [constructor, in ssralg]
GRing.QE.mixin_of [record, in ssralg]
GRing.QE.pack [definition, in ssralg]
GRing.QE.Pack [constructor, in ssralg]
GRing.QE.proj [projection, in ssralg]
GRing.QE.ringType [definition, in ssralg]
GRing.QE.sort [projection, in ssralg]
GRing.QE.type [record, in ssralg]
GRing.QE.unitRingType [definition, in ssralg]
GRing.QE.wf_proj [projection, in ssralg]
GRing.QE.wf_proj_axiom [definition, in ssralg]
GRing.QE.zmodType [definition, in ssralg]
GRing.qf_eval [definition, in ssralg]
GRing.qf_to_dnfP [lemma, in ssralg]
GRing.qf_to_dnf [definition, in ssralg]
GRing.qf_form [definition, in ssralg]
GRing.qf_evalP [lemma, in ssralg]
GRing.qf_to_dnf_rterm [lemma, in ssralg]
GRing.quantifier_elim_wf [lemma, in ssralg]
GRing.quantifier_elim [definition, in ssralg]
GRing.quantifier_elim_rformP [lemma, in ssralg]
GRing.raddfD [lemma, in ssralg]
GRing.raddfMn [lemma, in ssralg]
GRing.raddfMNn [lemma, in ssralg]
GRing.raddfN [lemma, in ssralg]
GRing.raddf_sub [lemma, in ssralg]
GRing.raddf_sum [lemma, in ssralg]
GRing.raddf0 [lemma, in ssralg]
GRing.regular [definition, in ssralg]
GRing.regular_fieldType [definition, in ssralg]
GRing.regular_idomainType [definition, in ssralg]
GRing.regular_unitAlgType [definition, in ssralg]
GRing.regular_comUnitRingType [definition, in ssralg]
GRing.regular_unitRingType [definition, in ssralg]
GRing.regular_algType [definition, in ssralg]
GRing.regular_comRingType [definition, in ssralg]
GRing.regular_lalgType [definition, in ssralg]
GRing.regular_lmodType [definition, in ssralg]
GRing.regular_ringType [definition, in ssralg]
GRing.regular_zmodType [definition, in ssralg]
GRing.regular_choiceType [definition, in ssralg]
GRing.regular_eqType [definition, in ssralg]
GRing.regular_lmodMixin [definition, in ssralg]
GRing.rev_unitrP [lemma, in ssralg]
GRing.rformula [definition, in ssralg]
GRing.RingTheory [section, in ssralg]
GRing.RingTheory.FrobeniusAutomorphism [section, in ssralg]
GRing.RingTheory.FrobeniusAutomorphism.charFp [variable, in ssralg]
GRing.RingTheory.FrobeniusAutomorphism.p [variable, in ssralg]
GRing.RingTheory.R [variable, in ssralg]
GRing.Ring.base [projection, in ssralg]
GRing.Ring.choiceType [definition, in ssralg]
GRing.Ring.Class [constructor, in ssralg]
GRing.Ring.class [definition, in ssralg]
GRing.Ring.ClassDef [section, in ssralg]
GRing.Ring.ClassDef.cT [variable, in ssralg]
GRing.Ring.ClassDef.T [variable, in ssralg]
GRing.Ring.class_of [record, in ssralg]
GRing.Ring.clone [definition, in ssralg]
GRing.Ring.eqType [definition, in ssralg]
GRing.Ring.EtaMixin [definition, in ssralg]
GRing.Ring.Exports.RingMixin [abbreviation, in ssralg]
GRing.Ring.Exports.ringType [abbreviation, in ssralg]
GRing.Ring.Exports.RingType [abbreviation, in ssralg]
GRing.Ring.Mixin [constructor, in ssralg]
GRing.Ring.mixin [projection, in ssralg]
GRing.Ring.mixin_of [record, in ssralg]
GRing.Ring.mul [projection, in ssralg]
GRing.Ring.one [projection, in ssralg]
GRing.Ring.Pack [constructor, in ssralg]
GRing.Ring.pack [definition, in ssralg]
GRing.Ring.sort [projection, in ssralg]
GRing.Ring.type [record, in ssralg]
GRing.Ring.zmodType [definition, in ssralg]
GRing.rmorphD [lemma, in ssralg]
GRing.rmorphismMP [lemma, in ssralg]
GRing.rmorphismP [lemma, in ssralg]
GRing.RmorphismTheory [section, in ssralg]
GRing.RmorphismTheory.InAlgebra [section, in ssralg]
GRing.RmorphismTheory.InAlgebra.A [variable, in ssralg]
GRing.RmorphismTheory.InAlgebra.R [variable, in ssralg]
GRing.RmorphismTheory.Projections [section, in ssralg]
GRing.RmorphismTheory.Projections.f [variable, in ssralg]
GRing.RmorphismTheory.Projections.g [variable, in ssralg]
GRing.RmorphismTheory.Projections.R [variable, in ssralg]
GRing.RmorphismTheory.Projections.S [variable, in ssralg]
GRing.RmorphismTheory.Projections.T [variable, in ssralg]
GRing.RmorphismTheory.Properties [section, in ssralg]
GRing.RmorphismTheory.Properties.f [variable, in ssralg]
GRing.RmorphismTheory.Properties.R [variable, in ssralg]
GRing.RmorphismTheory.Properties.S [variable, in ssralg]
GRing.RMorphism.additive [definition, in ssralg]
GRing.RMorphism.apply [projection, in ssralg]
GRing.RMorphism.base [projection, in ssralg]
GRing.RMorphism.Class [constructor, in ssralg]
GRing.RMorphism.class [definition, in ssralg]
GRing.RMorphism.ClassDef [section, in ssralg]
GRing.RMorphism.ClassDef.cF [variable, in ssralg]
GRing.RMorphism.ClassDef.f [variable, in ssralg]
GRing.RMorphism.ClassDef.g [variable, in ssralg]
GRing.RMorphism.ClassDef.phRS [variable, in ssralg]
GRing.RMorphism.ClassDef.R [variable, in ssralg]
GRing.RMorphism.ClassDef.S [variable, in ssralg]
GRing.RMorphism.class_of [record, in ssralg]
GRing.RMorphism.clone [definition, in ssralg]
GRing.RMorphism.Exports.AddRMorphism [abbreviation, in ssralg]
GRing.RMorphism.Exports.multiplicative [abbreviation, in ssralg]
GRing.RMorphism.Exports.rmorphism [abbreviation, in ssralg]
GRing.RMorphism.Exports.RMorphism [abbreviation, in ssralg]
GRing.RMorphism.map [record, in ssralg]
GRing.RMorphism.mixin [projection, in ssralg]
GRing.RMorphism.mixin_of [definition, in ssralg]
GRing.RMorphism.Pack [constructor, in ssralg]
GRing.RMorphism.pack [definition, in ssralg]
GRing.rmorphM [lemma, in ssralg]
GRing.rmorphMn [lemma, in ssralg]
GRing.rmorphMNn [lemma, in ssralg]
GRing.rmorphN [lemma, in ssralg]
GRing.rmorphV [lemma, in ssralg]
GRing.rmorphX [lemma, in ssralg]
GRing.rmorph_sub [lemma, in ssralg]
GRing.rmorph_comm [lemma, in ssralg]
GRing.rmorph_unit [lemma, in ssralg]
GRing.rmorph_prod [lemma, in ssralg]
GRing.rmorph_nat [lemma, in ssralg]
GRing.rmorph_sign [lemma, in ssralg]
GRing.rmorph_sum [lemma, in ssralg]
GRing.rmorph_div [lemma, in ssralg]
GRing.rmorph_char [lemma, in ssralg]
GRing.rmorph0 [lemma, in ssralg]
GRing.rmorph1 [lemma, in ssralg]
GRing.rterm [definition, in ssralg]
GRing.same_env [definition, in ssralg]
GRing.same_env_sym [lemma, in ssralg]
GRing.sat [definition, in ssralg]
GRing.satP [lemma, in ssralg]
GRing.scale [definition, in ssralg]
GRing.scaleNr [lemma, in ssralg]
GRing.scaleN1r [lemma, in ssralg]
GRing.scalerA [lemma, in ssralg]
GRing.scalerI [lemma, in ssralg]
GRing.scalerK [lemma, in ssralg]
GRing.scalerKV [lemma, in ssralg]
GRing.scalerN [lemma, in ssralg]
GRing.scaler_subr [lemma, in ssralg]
GRing.scaler_unit [lemma, in ssralg]
GRing.scaler_swap [lemma, in ssralg]
GRing.scaler_inv [lemma, in ssralg]
GRing.scaler_prod [lemma, in ssralg]
GRing.scaler_mulr [lemma, in ssralg]
GRing.scaler_subl [lemma, in ssralg]
GRing.scaler_eq0 [lemma, in ssralg]
GRing.scaler_sumr [lemma, in ssralg]
GRing.scaler_exp [lemma, in ssralg]
GRing.scaler_injl [lemma, in ssralg]
GRing.scaler_addl [lemma, in ssralg]
GRing.scaler_prodl [lemma, in ssralg]
GRing.scaler_prodr [lemma, in ssralg]
GRing.scaler_mull [lemma, in ssralg]
GRing.scaler_mulrnl [lemma, in ssralg]
GRing.scaler_mulrnr [lemma, in ssralg]
GRing.scaler_addr [lemma, in ssralg]
GRing.scaler_nat [lemma, in ssralg]
GRing.scaler_suml [lemma, in ssralg]
GRing.scaler0 [lemma, in ssralg]
GRing.scale_is_scalable [lemma, in ssralg]
GRing.scale_fun_linear [definition, in ssralg]
GRing.scale_linear [definition, in ssralg]
GRing.scale_additive [definition, in ssralg]
GRing.scale_fun_additive [definition, in ssralg]
GRing.scale_fun_head [definition, in ssralg]
GRing.scale_is_additive [lemma, in ssralg]
GRing.scale_fun_is_additive [lemma, in ssralg]
GRing.scale_fun_is_scalable [lemma, in ssralg]
GRing.scale0r [lemma, in ssralg]
GRing.scale1r [lemma, in ssralg]
GRing.signr_eq0 [lemma, in ssralg]
GRing.signr_odd [lemma, in ssralg]
GRing.signr_addb [lemma, in ssralg]
GRing.size_sol [lemma, in ssralg]
GRing.sol [definition, in ssralg]
GRing.solP [lemma, in ssralg]
GRing.solve_monicpoly [lemma, in ssralg]
GRing.sol_subproof [lemma, in ssralg]
GRing.sqrf_eq1 [lemma, in ssralg]
GRing.sqrrN [lemma, in ssralg]
GRing.sqrr_sub1 [lemma, in ssralg]
GRing.sqrr_add [lemma, in ssralg]
GRing.sqrr_sub [lemma, in ssralg]
GRing.sqrr_add1 [lemma, in ssralg]
GRing.subrK [definition, in ssralg]
GRing.subrr [definition, in ssralg]
GRing.subr_eq [lemma, in ssralg]
GRing.subr_sqr [lemma, in ssralg]
GRing.subr_sqr_1 [lemma, in ssralg]
GRing.subr_eq0 [lemma, in ssralg]
GRing.subr_sqr_add_sub [lemma, in ssralg]
GRing.subr_expn [lemma, in ssralg]
GRing.subr_expn_comm [lemma, in ssralg]
GRing.subr_expn_1 [lemma, in ssralg]
GRing.subr0 [lemma, in ssralg]
GRing.Substitution [section, in ssralg]
GRing.Substitution.R [variable, in ssralg]
GRing.sub_fun_linear [definition, in ssralg]
GRing.sub_fun_additive [definition, in ssralg]
GRing.sub_fun_is_scalable [lemma, in ssralg]
GRing.sub_fun_is_additive [lemma, in ssralg]
GRing.sub_fun_head [definition, in ssralg]
GRing.sub0r [lemma, in ssralg]
GRing.sumr_opp [lemma, in ssralg]
GRing.sumr_muln [lemma, in ssralg]
GRing.sumr_muln_r [lemma, in ssralg]
GRing.sumr_const [lemma, in ssralg]
GRing.sumr_sub [lemma, in ssralg]
GRing.term [inductive, in ssralg]
GRing.TermDef [section, in ssralg]
GRing.TermDef.R [variable, in ssralg]
GRing.Theory.addIr [definition, in ssralg]
GRing.Theory.addKr [definition, in ssralg]
GRing.Theory.addNKr [definition, in ssralg]
GRing.Theory.addNr [definition, in ssralg]
GRing.Theory.addrA [definition, in ssralg]
GRing.Theory.addrAC [definition, in ssralg]
GRing.Theory.addrC [definition, in ssralg]
GRing.Theory.addrCA [definition, in ssralg]
GRing.Theory.addrI [definition, in ssralg]
GRing.Theory.addrK [definition, in ssralg]
GRing.Theory.addrN [definition, in ssralg]
GRing.Theory.addrNK [definition, in ssralg]
GRing.Theory.addr_eq0 [definition, in ssralg]
GRing.Theory.addr0 [definition, in ssralg]
GRing.Theory.add0r [definition, in ssralg]
GRing.Theory.bij_linear [definition, in ssralg]
GRing.Theory.bij_additive [definition, in ssralg]
GRing.Theory.bij_rmorphism [definition, in ssralg]
GRing.Theory.bij_lrmorphism [definition, in ssralg]
GRing.Theory.bin_lt_charf_0 [definition, in ssralg]
GRing.Theory.can2_linear [definition, in ssralg]
GRing.Theory.can2_lrmorphism [definition, in ssralg]
GRing.Theory.can2_additive [definition, in ssralg]
GRing.Theory.can2_rmorphism [definition, in ssralg]
GRing.Theory.charf_prime [definition, in ssralg]
GRing.Theory.charf_eq [definition, in ssralg]
GRing.Theory.charf'_nat [definition, in ssralg]
GRing.Theory.charf0 [definition, in ssralg]
GRing.Theory.charf0P [definition, in ssralg]
GRing.Theory.char0_natf_div [definition, in ssralg]
GRing.Theory.commrN1 [definition, in ssralg]
GRing.Theory.commr_nat [definition, in ssralg]
GRing.Theory.commr_muln [definition, in ssralg]
GRing.Theory.commr_inv [definition, in ssralg]
GRing.Theory.commr_unit_mul [definition, in ssralg]
GRing.Theory.commr_exp [definition, in ssralg]
GRing.Theory.commr_sign [definition, in ssralg]
GRing.Theory.commr_sym [definition, in ssralg]
GRing.Theory.commr_opp [definition, in ssralg]
GRing.Theory.commr_add [definition, in ssralg]
GRing.Theory.commr_mul [definition, in ssralg]
GRing.Theory.commr_exp_mull [definition, in ssralg]
GRing.Theory.commr_refl [definition, in ssralg]
GRing.Theory.commr0 [definition, in ssralg]
GRing.Theory.commr1 [definition, in ssralg]
GRing.Theory.divff [definition, in ssralg]
GRing.Theory.divfK [definition, in ssralg]
GRing.Theory.divrK [definition, in ssralg]
GRing.Theory.divrr [definition, in ssralg]
GRing.Theory.divr1 [definition, in ssralg]
GRing.Theory.div1r [definition, in ssralg]
GRing.Theory.dvdn_charf [definition, in ssralg]
GRing.Theory.eqr_opp [definition, in ssralg]
GRing.Theory.eqr_oppC [definition, in ssralg]
GRing.Theory.eq_sol [definition, in ssralg]
GRing.Theory.eq_holds [definition, in ssralg]
GRing.Theory.eq_sat [definition, in ssralg]
GRing.Theory.eq_eval [definition, in ssralg]
GRing.Theory.eval_tsubst [definition, in ssralg]
GRing.Theory.expfS_eq1 [definition, in ssralg]
GRing.Theory.expf_eq0 [definition, in ssralg]
GRing.Theory.expf_neq0 [definition, in ssralg]
GRing.Theory.exprN [definition, in ssralg]
GRing.Theory.exprn_mulr [definition, in ssralg]
GRing.Theory.exprn_subl [definition, in ssralg]
GRing.Theory.exprn_dvd [definition, in ssralg]
GRing.Theory.exprn_mulnl [definition, in ssralg]
GRing.Theory.exprn_mull [definition, in ssralg]
GRing.Theory.exprn_addl_comm [definition, in ssralg]
GRing.Theory.exprn_subl_comm [definition, in ssralg]
GRing.Theory.exprn_addl [definition, in ssralg]
GRing.Theory.exprn_addr [definition, in ssralg]
GRing.Theory.exprn_mod [definition, in ssralg]
GRing.Theory.exprn_add1 [definition, in ssralg]
GRing.Theory.exprS [definition, in ssralg]
GRing.Theory.exprSr [definition, in ssralg]
GRing.Theory.expr_inv [definition, in ssralg]
GRing.Theory.expr0 [definition, in ssralg]
GRing.Theory.expr1 [definition, in ssralg]
GRing.Theory.expr2 [definition, in ssralg]
GRing.Theory.exp1rn [definition, in ssralg]
GRing.Theory.fmorphV [definition, in ssralg]
GRing.Theory.fmorph_eq0 [definition, in ssralg]
GRing.Theory.fmorph_div [definition, in ssralg]
GRing.Theory.fmorph_unit [definition, in ssralg]
GRing.Theory.fmorph_inj [definition, in ssralg]
GRing.Theory.fmorph_char [definition, in ssralg]
GRing.Theory.Frobenius_aut_sub_comm [definition, in ssralg]
GRing.Theory.Frobenius_aut_nat [definition, in ssralg]
GRing.Theory.Frobenius_aut_opp [definition, in ssralg]
GRing.Theory.Frobenius_aut_0 [definition, in ssralg]
GRing.Theory.Frobenius_aut_muln [definition, in ssralg]
GRing.Theory.Frobenius_aut_1 [definition, in ssralg]
GRing.Theory.Frobenius_aut_add_comm [definition, in ssralg]
GRing.Theory.Frobenius_autE [definition, in ssralg]
GRing.Theory.Frobenius_aut_exp [definition, in ssralg]
GRing.Theory.Frobenius_aut_mul_comm [definition, in ssralg]
GRing.Theory.holds_fsubst [definition, in ssralg]
GRing.Theory.invf_mul [definition, in ssralg]
GRing.Theory.invrK [definition, in ssralg]
GRing.Theory.invrN [definition, in ssralg]
GRing.Theory.invr_inj [definition, in ssralg]
GRing.Theory.invr_out [definition, in ssralg]
GRing.Theory.invr_mul [definition, in ssralg]
GRing.Theory.invr_eq0 [definition, in ssralg]
GRing.Theory.invr_neq0 [definition, in ssralg]
GRing.Theory.invr0 [definition, in ssralg]
GRing.Theory.invr1 [definition, in ssralg]
GRing.Theory.in_alg [abbreviation, in ssralg]
GRing.Theory.linearD [definition, in ssralg]
GRing.Theory.linearMn [definition, in ssralg]
GRing.Theory.linearMNn [definition, in ssralg]
GRing.Theory.linearN [definition, in ssralg]
GRing.Theory.linearP [definition, in ssralg]
GRing.Theory.linearZ [definition, in ssralg]
GRing.Theory.linear_sum [definition, in ssralg]
GRing.Theory.linear_sub [definition, in ssralg]
GRing.Theory.linear0 [definition, in ssralg]
GRing.Theory.mulfI [definition, in ssralg]
GRing.Theory.mulfK [definition, in ssralg]
GRing.Theory.mulfV [definition, in ssralg]
GRing.Theory.mulfVK [definition, in ssralg]
GRing.Theory.mulf_eq0 [definition, in ssralg]
GRing.Theory.mulf_neq0 [definition, in ssralg]
GRing.Theory.mulIf [definition, in ssralg]
GRing.Theory.mulIr [definition, in ssralg]
GRing.Theory.mulKf [definition, in ssralg]
GRing.Theory.mulKr [definition, in ssralg]
GRing.Theory.mulNr [definition, in ssralg]
GRing.Theory.mulNrn [definition, in ssralg]
GRing.Theory.mulN1r [definition, in ssralg]
GRing.Theory.mulrA [definition, in ssralg]
GRing.Theory.mulrAC [definition, in ssralg]
GRing.Theory.mulrb [definition, in ssralg]
GRing.Theory.mulrC [definition, in ssralg]
GRing.Theory.mulrCA [definition, in ssralg]
GRing.Theory.mulrI [definition, in ssralg]
GRing.Theory.mulrK [definition, in ssralg]
GRing.Theory.mulrN [definition, in ssralg]
GRing.Theory.mulrnA [definition, in ssralg]
GRing.Theory.mulrnAC [definition, in ssralg]
GRing.Theory.mulrnAl [definition, in ssralg]
GRing.Theory.mulrnAr [definition, in ssralg]
GRing.Theory.mulrNN [definition, in ssralg]
GRing.Theory.mulrn_addr [definition, in ssralg]
GRing.Theory.mulrn_subr [definition, in ssralg]
GRing.Theory.mulrn_addl [definition, in ssralg]
GRing.Theory.mulrn_subl [definition, in ssralg]
GRing.Theory.mulrN1 [definition, in ssralg]
GRing.Theory.mulrS [definition, in ssralg]
GRing.Theory.mulrSr [definition, in ssralg]
GRing.Theory.mulrV [definition, in ssralg]
GRing.Theory.mulrVK [definition, in ssralg]
GRing.Theory.mulr_addl [definition, in ssralg]
GRing.Theory.mulr_sumr [definition, in ssralg]
GRing.Theory.mulr_natr [definition, in ssralg]
GRing.Theory.mulr_addr [definition, in ssralg]
GRing.Theory.mulr_subl [definition, in ssralg]
GRing.Theory.mulr_suml [definition, in ssralg]
GRing.Theory.mulr_natl [definition, in ssralg]
GRing.Theory.mulr_subr [definition, in ssralg]
GRing.Theory.mulr0 [definition, in ssralg]
GRing.Theory.mulr0n [definition, in ssralg]
GRing.Theory.mulr1 [definition, in ssralg]
GRing.Theory.mulr1n [definition, in ssralg]
GRing.Theory.mulr2n [definition, in ssralg]
GRing.Theory.mulVf [definition, in ssralg]
GRing.Theory.mulVKf [definition, in ssralg]
GRing.Theory.mulVKr [definition, in ssralg]
GRing.Theory.mulVr [definition, in ssralg]
GRing.Theory.mul0r [definition, in ssralg]
GRing.Theory.mul0rn [definition, in ssralg]
GRing.Theory.mul1r [definition, in ssralg]
GRing.Theory.natf0_char [definition, in ssralg]
GRing.Theory.natr_add [definition, in ssralg]
GRing.Theory.natr_sub [definition, in ssralg]
GRing.Theory.natr_sum [definition, in ssralg]
GRing.Theory.natr_mul [definition, in ssralg]
GRing.Theory.natr_exp [definition, in ssralg]
GRing.Theory.natr_div [definition, in ssralg]
GRing.Theory.nonzero1r [definition, in ssralg]
GRing.Theory.null_fun [abbreviation, in ssralg]
GRing.Theory.oner_eq0 [definition, in ssralg]
GRing.Theory.opprK [definition, in ssralg]
GRing.Theory.oppr_eq0 [definition, in ssralg]
GRing.Theory.oppr_add [definition, in ssralg]
GRing.Theory.oppr_sub [definition, in ssralg]
GRing.Theory.oppr0 [definition, in ssralg]
GRing.Theory.prodf_inv [definition, in ssralg]
GRing.Theory.prodr_opp [definition, in ssralg]
GRing.Theory.prodr_exp_r [definition, in ssralg]
GRing.Theory.prodr_exp [definition, in ssralg]
GRing.Theory.prodr_const [definition, in ssralg]
GRing.Theory.raddfD [definition, in ssralg]
GRing.Theory.raddfMn [definition, in ssralg]
GRing.Theory.raddfMNn [definition, in ssralg]
GRing.Theory.raddfN [definition, in ssralg]
GRing.Theory.raddf_sub [definition, in ssralg]
GRing.Theory.raddf_sum [definition, in ssralg]
GRing.Theory.raddf0 [definition, in ssralg]
GRing.Theory.rmorphD [definition, in ssralg]
GRing.Theory.rmorphismMP [definition, in ssralg]
GRing.Theory.rmorphismP [definition, in ssralg]
GRing.Theory.rmorphM [definition, in ssralg]
GRing.Theory.rmorphMn [definition, in ssralg]
GRing.Theory.rmorphMNn [definition, in ssralg]
GRing.Theory.rmorphN [definition, in ssralg]
GRing.Theory.rmorphV [definition, in ssralg]
GRing.Theory.rmorphX [definition, in ssralg]
GRing.Theory.rmorph_comm [definition, in ssralg]
GRing.Theory.rmorph_prod [definition, in ssralg]
GRing.Theory.rmorph_sum [definition, in ssralg]
GRing.Theory.rmorph_div [definition, in ssralg]
GRing.Theory.rmorph_nat [definition, in ssralg]
GRing.Theory.rmorph_sub [definition, in ssralg]
GRing.Theory.rmorph_char [definition, in ssralg]
GRing.Theory.rmorph_unit [definition, in ssralg]
GRing.Theory.rmorph_sign [definition, in ssralg]
GRing.Theory.rmorph0 [definition, in ssralg]
GRing.Theory.rmorph1 [definition, in ssralg]
GRing.Theory.satP [definition, in ssralg]
GRing.Theory.scaleNr [definition, in ssralg]
GRing.Theory.scaleN1r [definition, in ssralg]
GRing.Theory.scalerA [definition, in ssralg]
GRing.Theory.scalerI [definition, in ssralg]
GRing.Theory.scalerK [definition, in ssralg]
GRing.Theory.scalerKV [definition, in ssralg]
GRing.Theory.scalerN [definition, in ssralg]
GRing.Theory.scaler_injl [definition, in ssralg]
GRing.Theory.scaler_eq0 [definition, in ssralg]
GRing.Theory.scaler_prod [definition, in ssralg]
GRing.Theory.scaler_exp [definition, in ssralg]
GRing.Theory.scaler_sumr [definition, in ssralg]
GRing.Theory.scaler_swap [definition, in ssralg]
GRing.Theory.scaler_suml [definition, in ssralg]
GRing.Theory.scaler_mulr [definition, in ssralg]
GRing.Theory.scaler_mull [definition, in ssralg]
GRing.Theory.scaler_mulrnl [definition, in ssralg]
GRing.Theory.scaler_nat [definition, in ssralg]
GRing.Theory.scaler_addl [definition, in ssralg]
GRing.Theory.scaler_prodl [definition, in ssralg]
GRing.Theory.scaler_mulrnr [definition, in ssralg]
GRing.Theory.scaler_subr [definition, in ssralg]
GRing.Theory.scaler_addr [definition, in ssralg]
GRing.Theory.scaler_inv [definition, in ssralg]
GRing.Theory.scaler_subl [definition, in ssralg]
GRing.Theory.scaler_unit [definition, in ssralg]
GRing.Theory.scaler_prodr [definition, in ssralg]
GRing.Theory.scaler0 [definition, in ssralg]
GRing.Theory.scale0r [definition, in ssralg]
GRing.Theory.scale1r [definition, in ssralg]
GRing.Theory.signr_addb [definition, in ssralg]
GRing.Theory.signr_odd [definition, in ssralg]
GRing.Theory.signr_eq0 [definition, in ssralg]
GRing.Theory.size_sol [definition, in ssralg]
GRing.Theory.solP [definition, in ssralg]
GRing.Theory.solve_monicpoly [definition, in ssralg]
GRing.Theory.sqrf_eq1 [definition, in ssralg]
GRing.Theory.sqrrN [definition, in ssralg]
GRing.Theory.sqrr_add [definition, in ssralg]
GRing.Theory.sqrr_sub [definition, in ssralg]
GRing.Theory.sqrr_add1 [definition, in ssralg]
GRing.Theory.sqrr_sub1 [definition, in ssralg]
GRing.Theory.subrK [definition, in ssralg]
GRing.Theory.subrr [definition, in ssralg]
GRing.Theory.subr_eq [definition, in ssralg]
GRing.Theory.subr_sqr [definition, in ssralg]
GRing.Theory.subr_sqr_add_sub [definition, in ssralg]
GRing.Theory.subr_expn_comm [definition, in ssralg]
GRing.Theory.subr_sqr_1 [definition, in ssralg]
GRing.Theory.subr_expn_1 [definition, in ssralg]
GRing.Theory.subr_expn [definition, in ssralg]
GRing.Theory.subr_eq0 [definition, in ssralg]
GRing.Theory.subr0 [definition, in ssralg]
GRing.Theory.sub0r [definition, in ssralg]
GRing.Theory.sumr_muln [definition, in ssralg]
GRing.Theory.sumr_const [definition, in ssralg]
GRing.Theory.sumr_muln_r [definition, in ssralg]
GRing.Theory.sumr_opp [definition, in ssralg]
GRing.Theory.sumr_sub [definition, in ssralg]
GRing.Theory.unitfE [definition, in ssralg]
GRing.Theory.unitrE [definition, in ssralg]
GRing.Theory.unitrP [definition, in ssralg]
GRing.Theory.unitr_pexp [definition, in ssralg]
GRing.Theory.unitr_inv [definition, in ssralg]
GRing.Theory.unitr_mull [definition, in ssralg]
GRing.Theory.unitr_opp [definition, in ssralg]
GRing.Theory.unitr_exp [definition, in ssralg]
GRing.Theory.unitr_mul [definition, in ssralg]
GRing.Theory.unitr_mulr [definition, in ssralg]
GRing.Theory.unitr0 [definition, in ssralg]
GRing.Theory.unitr1 [definition, in ssralg]
GRing.to_rform_rformula [lemma, in ssralg]
GRing.to_rterm_id [lemma, in ssralg]
GRing.to_rterm [definition, in ssralg]
GRing.to_rformP [lemma, in ssralg]
GRing.to_rform [definition, in ssralg]
GRing.True [abbreviation, in ssralg]
GRing.tsubst [definition, in ssralg]
GRing.ub_var [definition, in ssralg]
GRing.Unit [constructor, in ssralg]
GRing.unit [definition, in ssralg]
GRing.UnitAlgebraTheory [section, in ssralg]
GRing.UnitAlgebraTheory.A [variable, in ssralg]
GRing.UnitAlgebraTheory.R [variable, in ssralg]
GRing.UnitAlgebra.algType [definition, in ssralg]
GRing.UnitAlgebra.alg_unitRingType [definition, in ssralg]
GRing.UnitAlgebra.base [projection, in ssralg]
GRing.UnitAlgebra.base2 [definition, in ssralg]
GRing.UnitAlgebra.choiceType [definition, in ssralg]
GRing.UnitAlgebra.class [definition, in ssralg]
GRing.UnitAlgebra.Class [constructor, in ssralg]
GRing.UnitAlgebra.ClassDef [section, in ssralg]
GRing.UnitAlgebra.ClassDef.cT [variable, in ssralg]
GRing.UnitAlgebra.ClassDef.phR [variable, in ssralg]
GRing.UnitAlgebra.ClassDef.R [variable, in ssralg]
GRing.UnitAlgebra.ClassDef.T [variable, in ssralg]
GRing.UnitAlgebra.class_of [record, in ssralg]
GRing.UnitAlgebra.eqType [definition, in ssralg]
GRing.UnitAlgebra.Exports.unitAlgType [abbreviation, in ssralg]
GRing.UnitAlgebra.lalgType [definition, in ssralg]
GRing.UnitAlgebra.lalg_unitRingType [definition, in ssralg]
GRing.UnitAlgebra.lmodType [definition, in ssralg]
GRing.UnitAlgebra.lmod_unitRingType [definition, in ssralg]
GRing.UnitAlgebra.mixin [projection, in ssralg]
GRing.UnitAlgebra.Pack [constructor, in ssralg]
GRing.UnitAlgebra.pack [definition, in ssralg]
GRing.UnitAlgebra.ringType [definition, in ssralg]
GRing.UnitAlgebra.sort [projection, in ssralg]
GRing.UnitAlgebra.type [record, in ssralg]
GRing.UnitAlgebra.unitRingType [definition, in ssralg]
GRing.UnitAlgebra.zmodType [definition, in ssralg]
GRing.unitfE [lemma, in ssralg]
GRing.unitrE [lemma, in ssralg]
GRing.UnitRingMorphism [section, in ssralg]
GRing.UnitRingMorphism.f [variable, in ssralg]
GRing.UnitRingMorphism.R [variable, in ssralg]
GRing.UnitRingMorphism.S [variable, in ssralg]
GRing.UnitRingTheory [section, in ssralg]
GRing.UnitRingTheory.R [variable, in ssralg]
GRing.UnitRing.base [projection, in ssralg]
GRing.UnitRing.choiceType [definition, in ssralg]
GRing.UnitRing.Class [constructor, in ssralg]
GRing.UnitRing.class [definition, in ssralg]
GRing.UnitRing.ClassDef [section, in ssralg]
GRing.UnitRing.ClassDef.cT [variable, in ssralg]
GRing.UnitRing.ClassDef.T [variable, in ssralg]
GRing.UnitRing.class_of [record, in ssralg]
GRing.UnitRing.clone [definition, in ssralg]
GRing.UnitRing.eqType [definition, in ssralg]
GRing.UnitRing.EtaMixin [definition, in ssralg]
GRing.UnitRing.Exports.UnitRingMixin [abbreviation, in ssralg]
GRing.UnitRing.Exports.unitRingType [abbreviation, in ssralg]
GRing.UnitRing.Exports.UnitRingType [abbreviation, in ssralg]
GRing.UnitRing.inv [projection, in ssralg]
GRing.UnitRing.Mixin [constructor, in ssralg]
GRing.UnitRing.mixin [projection, in ssralg]
GRing.UnitRing.mixin_of [record, in ssralg]
GRing.UnitRing.Pack [constructor, in ssralg]
GRing.UnitRing.pack [definition, in ssralg]
GRing.UnitRing.ringType [definition, in ssralg]
GRing.UnitRing.sort [projection, in ssralg]
GRing.UnitRing.type [record, in ssralg]
GRing.UnitRing.unit [projection, in ssralg]
GRing.UnitRing.zmodType [definition, in ssralg]
GRing.unitrP [lemma, in ssralg]
GRing.unitr_mul [lemma, in ssralg]
GRing.unitr_opp [lemma, in ssralg]
GRing.unitr_pexp [lemma, in ssralg]
GRing.unitr_exp [lemma, in ssralg]
GRing.unitr_mulr [lemma, in ssralg]
GRing.unitr_mull [lemma, in ssralg]
GRing.unitr_inv [lemma, in ssralg]
GRing.unitr0 [lemma, in ssralg]
GRing.unitr1 [lemma, in ssralg]
GRing.Var [constructor, in ssralg]
GRing.wf_proj [lemma, in ssralg]
GRing.zero [definition, in ssralg]
GRing.ZmoduleTheory [section, in ssralg]
GRing.ZmoduleTheory.V [variable, in ssralg]
GRing.Zmodule.add [projection, in ssralg]
GRing.Zmodule.base [projection, in ssralg]
GRing.Zmodule.choiceType [definition, in ssralg]
GRing.Zmodule.Class [constructor, in ssralg]
GRing.Zmodule.class [definition, in ssralg]
GRing.Zmodule.ClassDef [section, in ssralg]
GRing.Zmodule.ClassDef.cT [variable, in ssralg]
GRing.Zmodule.ClassDef.T [variable, in ssralg]
GRing.Zmodule.class_of [record, in ssralg]
GRing.Zmodule.clone [definition, in ssralg]
GRing.Zmodule.eqType [definition, in ssralg]
GRing.Zmodule.Exports.ZmodMixin [abbreviation, in ssralg]
GRing.Zmodule.Exports.zmodType [abbreviation, in ssralg]
GRing.Zmodule.Exports.ZmodType [abbreviation, in ssralg]
GRing.Zmodule.mixin [projection, in ssralg]
GRing.Zmodule.Mixin [constructor, in ssralg]
GRing.Zmodule.mixin_of [record, in ssralg]
GRing.Zmodule.opp [projection, in ssralg]
GRing.Zmodule.Pack [constructor, in ssralg]
GRing.Zmodule.pack [definition, in ssralg]
GRing.Zmodule.sort [projection, in ssralg]
GRing.Zmodule.type [record, in ssralg]
GRing.Zmodule.zero [projection, in ssralg]
group [definition, in fingroup]
Group [constructor, in fingroup]
GroupAction [constructor, in action]
GroupAction [section, in action]
groupAction [record, in action]
GroupActionDefs [section, in action]
GroupActionDefs.aT [variable, in action]
GroupActionDefs.D [variable, in action]
GroupActionDefs.R [variable, in action]
GroupActionDefs.rT [variable, in action]
GroupActionTheory [section, in action]
GroupActionTheory.ActBy [section, in action]
GroupActionTheory.ActBy.A [variable, in action]
GroupActionTheory.ActBy.G [variable, in action]
GroupActionTheory.ActBy.nGAg [variable, in action]
GroupActionTheory.aT [variable, in action]
GroupActionTheory.CompAct [section, in action]
GroupActionTheory.CompAct.f [variable, in action]
GroupActionTheory.CompAct.G [variable, in action]
GroupActionTheory.CompAct.gT [variable, in action]
GroupActionTheory.D [variable, in action]
GroupActionTheory.Mod [section, in action]
GroupActionTheory.Mod.H [variable, in action]
GroupActionTheory.Quotient [section, in action]
GroupActionTheory.Quotient.H [variable, in action]
GroupActionTheory.R [variable, in action]
GroupActionTheory.Restrict [section, in action]
GroupActionTheory.Restrict.A [variable, in action]
GroupActionTheory.Restrict.sAD [variable, in action]
GroupActionTheory.rT [variable, in action]
GroupActionTheory.to [variable, in action]
GroupAction.aT [variable, in action]
GroupAction.D [variable, in action]
GroupAction.R [variable, in action]
GroupAction.rT [variable, in action]
groupCl [definition, in mxrepresentation]
GroupDefs [section, in gseries]
GroupDefs.gT [variable, in gseries]
groupD1_inj [lemma, in fingroup]
GroupIdentities [section, in fingroup]
GroupIdentities.T [variable, in fingroup]
GroupInter [section, in fingroup]
GroupInter.gT [variable, in fingroup]
GroupInter.Nary [section, in fingroup]
GroupInter.Nary.F [variable, in fingroup]
GroupInter.Nary.I [variable, in fingroup]
GroupInter.Nary.P [variable, in fingroup]
groupJ [lemma, in fingroup]
groupJr [lemma, in fingroup]
groupM [lemma, in fingroup]
groupMl [lemma, in fingroup]
groupMr [lemma, in fingroup]
groupP [lemma, in fingroup]
GroupProp [section, in fingroup]
GroupProp.gT [variable, in fingroup]
GroupProp.OneGroup [section, in fingroup]
GroupProp.OneGroup.G [variable, in fingroup]
groupR [lemma, in fingroup]
Groups [section, in zmodp]
GroupScope [module, in fingroup]
GroupSet [module, in fingroup]
GroupSetBaseGroup [module, in fingroup]
GroupSetBaseGroupSig [module, in fingroup]
GroupSetBaseGroupSig.sort [definition, in fingroup]
GroupSetMulDef [section, in fingroup]
GroupSetMulDef.gT [variable, in fingroup]
GroupSetMulProp [section, in fingroup]
GroupSetMulProp.gT [variable, in fingroup]
GroupSet.sort [definition, in fingroup]
Groups.p [variable, in zmodp]
groupT [abbreviation, in fingroup]
groupT [abbreviation, in gseries]
groupV [lemma, in fingroup]
groupVl [lemma, in fingroup]
groupVr [lemma, in fingroup]
groupX [lemma, in fingroup]
group_of [definition, in fingroup]
group_closure_field_exists [lemma, in mxrepresentation]
group_type [record, in fingroup]
group_setT [lemma, in fingroup]
group_splitting_field [definition, in mxrepresentation]
group_of_subFinType [definition, in fingroup]
group_of_finType [definition, in fingroup]
group_of_subCountType [definition, in fingroup]
group_of_countType [definition, in fingroup]
group_of_choiceType [definition, in fingroup]
group_of_eqType [definition, in fingroup]
group_of_subType [definition, in fingroup]
group_subFinType [definition, in fingroup]
group_finType [definition, in fingroup]
group_subCountType [definition, in fingroup]
group_countType [definition, in fingroup]
group_choiceType [definition, in fingroup]
group_eqType [definition, in fingroup]
group_subType [definition, in fingroup]
group_set_finType [definition, in fingroup]
group_set_countType [definition, in fingroup]
group_set_choiceType [definition, in fingroup]
group_set_eqType [definition, in fingroup]
group_set_of_baseGroupType [definition, in fingroup]
group_set_baseGroupType [definition, in fingroup]
group_rel_of [definition, in gseries]
group_finMixin [definition, in fingroup]
group_setP [lemma, in fingroup]
group_set_gacent [lemma, in action]
group_closure_field [definition, in mxrepresentation]
group_set_astab [lemma, in action]
group_countMixin [definition, in fingroup]
group_setX [lemma, in gproduct]
group_set_astabs [lemma, in action]
group_not0 [lemma, in gproduct]
group_set_conjG [lemma, in fingroup]
group_splitting_field_exists [lemma, in mxrepresentation]
group_modl [lemma, in fingroup]
group_set_normaliser [lemma, in fingroup]
group_ring [definition, in mxrepresentation]
group_Ldiv [lemma, in abelian]
group_set_baseGroupMixin [definition, in fingroup]
group_set_one [lemma, in fingroup]
group_choiceMixin [definition, in fingroup]
group_prod [lemma, in fingroup]
group_eqMixin [definition, in fingroup]
group_setI [lemma, in fingroup]
group_modr [lemma, in fingroup]
group_inj [lemma, in fingroup]
group_set_bigcap [lemma, in fingroup]
group_set [definition, in fingroup]
group0 [lemma, in gproduct]
group1 [lemma, in fingroup]
group1_class12 [lemma, in fingroup]
group1_finType [lemma, in fingroup]
group1_contra [lemma, in fingroup]
group1_class2 [lemma, in fingroup]
group1_class1 [lemma, in fingroup]
group1_eqType [lemma, in fingroup]
GrpQ [definition, in extremal]
Grp_dihedral [lemma, in extremal]
Grp_quaternion [lemma, in extremal]
Grp_modular_group [lemma, in extremal]
Grp_2dihedral [lemma, in extremal]
Grp_ext_dihedral [lemma, in extremal]
Grp_pX1p2 [lemma, in extraspecial]
Grp_semidihedral [lemma, in extremal]
Grp'_dihedral [lemma, in extremal]
gseries [library]
gset_mx [definition, in mxrepresentation]
gsimp [definition, in fingroup]
gsort [abbreviation, in fingroup]
gT [abbreviation, in action]
gTg [abbreviation, in jordanholder]
gtn [definition, in ssrnat]
gtnNdvd [lemma, in div]
GtnNotLeq [constructor, in ssrnat]
gTr [abbreviation, in fingroup]
gtype [abbreviation, in extraspecial]
gt_ [definition, in center]
gval [projection, in fingroup]
gzZ [definition, in center]
gzZchar [definition, in center]
gzZ_lone [definition, in center]
G_ [definition, in center]
G_ [abbreviation, in center]
G' [abbreviation, in hall]



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (14626 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (165 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (112 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (7292 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (761 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (250 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (390 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (84 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (3144 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (126 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (28 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (2221 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (53 entries)