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 (definition)

gacent [in action]
gacent_group [in action]
gact_range [in action]
gaussian_elimination [in mxalgebra]
gcdn [in div]
gcdn_addoid [in bigop]
gcdn_comoid [in bigop]
gcdn_monoid [in bigop]
gcdn_rec [in div]
gcdp [in poly]
gcore [in fingroup]
gcore_group [in fingroup]
Gcycg [in finmodule]
generated [in fingroup]
generated_group [in fingroup]
generator [in cyclic]
genmx [in mxalgebra]
genmx_witness [in mxalgebra]
genmx_def [in mxalgebra]
genmx_witnessP [in mxalgebra]
gen_rank [in abelian]
geq [in ssrnat]
gFcomp_mgFun [in gfunctor]
gFcomp_gFun [in gfunctor]
gFcomp_igFun [in gfunctor]
gFgroup [in gfunctor]
gFmod_pgFun [in gfunctor]
gFmod_gFun [in gfunctor]
gFmod_igFun [in gfunctor]
gFmod_group [in gfunctor]
GFunctor.clone [in gfunctor]
GFunctor.clone_mono [in gfunctor]
GFunctor.clone_pmap [in gfunctor]
GFunctor.clone_iso [in gfunctor]
GFunctor.closed [in gfunctor]
GFunctor.comp_head [in gfunctor]
GFunctor.continuous [in gfunctor]
GFunctor.group_valued [in gfunctor]
GFunctor.hereditary [in gfunctor]
GFunctor.iso_continuous [in gfunctor]
GFunctor.modulo [in gfunctor]
GFunctor.monotonic [in gfunctor]
GFunctor.object_map [in gfunctor]
GFunctor.pack_iso [in gfunctor]
GFunctor.pcontinuous [in gfunctor]
gFunc_id [in gfunctor]
gH [in center]
gK [in center]
GLgroup [in matrix]
GLgroup_group [in matrix]
GLrepr [in mxabelem]
GLtype [in matrix]
GLval [in matrix]
GL_eqMixin [in matrix]
GL_finGroupType [in matrix]
GL_baseFinGroupType [in matrix]
GL_subFinType [in matrix]
GL_finType [in matrix]
GL_subCountType [in matrix]
GL_countType [in matrix]
GL_choiceType [in matrix]
GL_eqType [in matrix]
GL_subType [in matrix]
gnorm [in fingroup]
gring_op [in mxrepresentation]
gring_index [in mxrepresentation]
gring_op_linear [in mxrepresentation]
gring_mx_linear [in mxrepresentation]
gring_proj_linear [in mxrepresentation]
gring_row_linear [in mxrepresentation]
gring_mx [in mxrepresentation]
gring_row [in mxrepresentation]
gring_proj [in mxrepresentation]
GRing.add [in ssralg]
GRing.Additive.axiom [in ssralg]
GRing.Additive.class [in ssralg]
GRing.Additive.clone [in ssralg]
GRing.addoid [in ssralg]
GRing.add_fun_linear [in ssralg]
GRing.add_fun_additive [in ssralg]
GRing.add_comoid [in ssralg]
GRing.add_monoid [in ssralg]
GRing.add_fun_head [in ssralg]
GRing.Algebra.axiom [in ssralg]
GRing.Algebra.choiceType [in ssralg]
GRing.Algebra.class [in ssralg]
GRing.Algebra.clone [in ssralg]
GRing.Algebra.eqType [in ssralg]
GRing.Algebra.lalgType [in ssralg]
GRing.Algebra.lmodType [in ssralg]
GRing.Algebra.pack [in ssralg]
GRing.Algebra.ringType [in ssralg]
GRing.Algebra.zmodType [in ssralg]
GRing.and_dnf [in ssralg]
GRing.char [in ssralg]
GRing.ClosedField.axiom [in ssralg]
GRing.ClosedField.choiceType [in ssralg]
GRing.ClosedField.class [in ssralg]
GRing.ClosedField.clone [in ssralg]
GRing.ClosedField.comRingType [in ssralg]
GRing.ClosedField.comUnitRingType [in ssralg]
GRing.ClosedField.decFieldType [in ssralg]
GRing.ClosedField.eqType [in ssralg]
GRing.ClosedField.fieldType [in ssralg]
GRing.ClosedField.idomainType [in ssralg]
GRing.ClosedField.pack [in ssralg]
GRing.ClosedField.ringType [in ssralg]
GRing.ClosedField.unitRingType [in ssralg]
GRing.ClosedField.zmodType [in ssralg]
GRing.comm [in ssralg]
GRing.comp_linear [in ssralg]
GRing.comp_rmorphism [in ssralg]
GRing.comp_additive [in ssralg]
GRing.comp_lrmorphism [in ssralg]
GRing.comp_is_multiplicative [in ssralg]
GRing.ComRing.choiceType [in ssralg]
GRing.ComRing.class [in ssralg]
GRing.ComRing.clone [in ssralg]
GRing.ComRing.eqType [in ssralg]
GRing.ComRing.pack [in ssralg]
GRing.ComRing.RingMixin [in ssralg]
GRing.ComRing.ringType [in ssralg]
GRing.ComRing.zmodType [in ssralg]
GRing.ComUnitRing.base2 [in ssralg]
GRing.ComUnitRing.choiceType [in ssralg]
GRing.ComUnitRing.class [in ssralg]
GRing.ComUnitRing.comRingType [in ssralg]
GRing.ComUnitRing.com_unitRingType [in ssralg]
GRing.ComUnitRing.eqType [in ssralg]
GRing.ComUnitRing.Mixin [in ssralg]
GRing.ComUnitRing.pack [in ssralg]
GRing.ComUnitRing.ringType [in ssralg]
GRing.ComUnitRing.unitRingType [in ssralg]
GRing.ComUnitRing.zmodType [in ssralg]
GRing.converse [in ssralg]
GRing.converse_ringMixin [in ssralg]
GRing.converse_unitRingType [in ssralg]
GRing.converse_ringType [in ssralg]
GRing.converse_zmodType [in ssralg]
GRing.converse_choiceType [in ssralg]
GRing.converse_eqType [in ssralg]
GRing.converse_unitRingMixin [in ssralg]
GRing.DecidableField.axiom [in ssralg]
GRing.DecidableField.choiceType [in ssralg]
GRing.DecidableField.class [in ssralg]
GRing.DecidableField.clone [in ssralg]
GRing.DecidableField.comRingType [in ssralg]
GRing.DecidableField.comUnitRingType [in ssralg]
GRing.DecidableField.eqType [in ssralg]
GRing.DecidableField.fieldType [in ssralg]
GRing.DecidableField.idomainType [in ssralg]
GRing.DecidableField.pack [in ssralg]
GRing.DecidableField.ringType [in ssralg]
GRing.DecidableField.unitRingType [in ssralg]
GRing.DecidableField.zmodType [in ssralg]
GRing.divfK [in ssralg]
GRing.divrK [in ssralg]
GRing.dnf_to_form [in ssralg]
GRing.dnf_rterm [in ssralg]
GRing.elim_aux [in ssralg]
GRing.eq0_rform [in ssralg]
GRing.eval [in ssralg]
GRing.exp [in ssralg]
GRing.Field.axiom [in ssralg]
GRing.Field.choiceType [in ssralg]
GRing.Field.class [in ssralg]
GRing.Field.clone [in ssralg]
GRing.Field.comRingType [in ssralg]
GRing.Field.comUnitRingType [in ssralg]
GRing.Field.eqType [in ssralg]
GRing.Field.idomainType [in ssralg]
GRing.Field.mixin_of [in ssralg]
GRing.Field.pack [in ssralg]
GRing.Field.ringType [in ssralg]
GRing.Field.UnitMixin [in ssralg]
GRing.Field.unitRingType [in ssralg]
GRing.Field.zmodType [in ssralg]
GRing.Frobenius_aut_rmorphism [in ssralg]
GRing.Frobenius_aut_additive [in ssralg]
GRing.Frobenius_aut [in ssralg]
GRing.fsubst [in ssralg]
GRing.holds [in ssralg]
GRing.idfun_linear [in ssralg]
GRing.idfun_rmorphism [in ssralg]
GRing.idfun_additive [in ssralg]
GRing.idfun_lrmorphism [in ssralg]
GRing.IntegralDomain.axiom [in ssralg]
GRing.IntegralDomain.choiceType [in ssralg]
GRing.IntegralDomain.class [in ssralg]
GRing.IntegralDomain.clone [in ssralg]
GRing.IntegralDomain.comRingType [in ssralg]
GRing.IntegralDomain.comUnitRingType [in ssralg]
GRing.IntegralDomain.eqType [in ssralg]
GRing.IntegralDomain.pack [in ssralg]
GRing.IntegralDomain.ringType [in ssralg]
GRing.IntegralDomain.unitRingType [in ssralg]
GRing.IntegralDomain.zmodType [in ssralg]
GRing.inv [in ssralg]
GRing.in_alg_rmorphism [in ssralg]
GRing.in_alg_additive [in ssralg]
GRing.in_alg_head [in ssralg]
GRing.Lalgebra.axiom [in ssralg]
GRing.Lalgebra.base2 [in ssralg]
GRing.Lalgebra.choiceType [in ssralg]
GRing.Lalgebra.class [in ssralg]
GRing.Lalgebra.clone [in ssralg]
GRing.Lalgebra.eqType [in ssralg]
GRing.Lalgebra.lmodType [in ssralg]
GRing.Lalgebra.lmod_ringType [in ssralg]
GRing.Lalgebra.pack [in ssralg]
GRing.Lalgebra.ringType [in ssralg]
GRing.Lalgebra.zmodType [in ssralg]
GRing.Linear.additive [in ssralg]
GRing.Linear.axiom [in ssralg]
GRing.Linear.class [in ssralg]
GRing.Linear.clone [in ssralg]
GRing.Linear.mixin_of [in ssralg]
GRing.Linear.pack [in ssralg]
GRing.Lmodule.choiceType [in ssralg]
GRing.Lmodule.class [in ssralg]
GRing.Lmodule.clone [in ssralg]
GRing.Lmodule.eqType [in ssralg]
GRing.Lmodule.pack [in ssralg]
GRing.Lmodule.zmodType [in ssralg]
GRing.LRMorphism.additive [in ssralg]
GRing.LRMorphism.base2 [in ssralg]
GRing.LRMorphism.class [in ssralg]
GRing.LRMorphism.clone [in ssralg]
GRing.LRMorphism.join_linear [in ssralg]
GRing.LRMorphism.join_rmorphism [in ssralg]
GRing.LRMorphism.linear [in ssralg]
GRing.LRMorphism.pack [in ssralg]
GRing.LRMorphism.rmorphism [in ssralg]
GRing.mul [in ssralg]
GRing.mulfV [in ssralg]
GRing.mull_fun_linear [in ssralg]
GRing.mull_fun_additive [in ssralg]
GRing.mull_fun_head [in ssralg]
GRing.muloid [in ssralg]
GRing.mulrV [in ssralg]
GRing.mulr_fun_linear [in ssralg]
GRing.mulr_fun_additive [in ssralg]
GRing.mulr_fun_head [in ssralg]
GRing.mul_comoid [in ssralg]
GRing.mul_monoid [in ssralg]
GRing.natmul [in ssralg]
GRing.natr_sum [in ssralg]
GRing.null_fun_linear [in ssralg]
GRing.null_fun_additive [in ssralg]
GRing.null_fun_head [in ssralg]
GRing.one [in ssralg]
GRing.opp [in ssralg]
GRing.opp_linear [in ssralg]
GRing.opp_additive [in ssralg]
GRing.Pick [in ssralg]
GRing.proj [in ssralg]
GRing.proj_sat [in ssralg]
GRing.QEDecidableField [in ssralg]
GRing.QEDecidableFieldMixin [in ssralg]
GRing.QE.choiceType [in ssralg]
GRing.QE.class [in ssralg]
GRing.QE.clone [in ssralg]
GRing.QE.comRingType [in ssralg]
GRing.QE.comUnitRingType [in ssralg]
GRing.QE.eqType [in ssralg]
GRing.QE.fieldType [in ssralg]
GRing.QE.holds_proj_axiom [in ssralg]
GRing.QE.idomainType [in ssralg]
GRing.QE.pack [in ssralg]
GRing.QE.ringType [in ssralg]
GRing.QE.unitRingType [in ssralg]
GRing.QE.wf_proj_axiom [in ssralg]
GRing.QE.zmodType [in ssralg]
GRing.qf_eval [in ssralg]
GRing.qf_to_dnf [in ssralg]
GRing.qf_form [in ssralg]
GRing.quantifier_elim [in ssralg]
GRing.regular [in ssralg]
GRing.regular_fieldType [in ssralg]
GRing.regular_idomainType [in ssralg]
GRing.regular_unitAlgType [in ssralg]
GRing.regular_comUnitRingType [in ssralg]
GRing.regular_unitRingType [in ssralg]
GRing.regular_algType [in ssralg]
GRing.regular_comRingType [in ssralg]
GRing.regular_lalgType [in ssralg]
GRing.regular_lmodType [in ssralg]
GRing.regular_ringType [in ssralg]
GRing.regular_zmodType [in ssralg]
GRing.regular_choiceType [in ssralg]
GRing.regular_eqType [in ssralg]
GRing.regular_lmodMixin [in ssralg]
GRing.rformula [in ssralg]
GRing.Ring.choiceType [in ssralg]
GRing.Ring.class [in ssralg]
GRing.Ring.clone [in ssralg]
GRing.Ring.eqType [in ssralg]
GRing.Ring.EtaMixin [in ssralg]
GRing.Ring.pack [in ssralg]
GRing.Ring.zmodType [in ssralg]
GRing.RMorphism.additive [in ssralg]
GRing.RMorphism.class [in ssralg]
GRing.RMorphism.clone [in ssralg]
GRing.RMorphism.mixin_of [in ssralg]
GRing.RMorphism.pack [in ssralg]
GRing.rterm [in ssralg]
GRing.same_env [in ssralg]
GRing.sat [in ssralg]
GRing.scale [in ssralg]
GRing.scale_fun_linear [in ssralg]
GRing.scale_linear [in ssralg]
GRing.scale_additive [in ssralg]
GRing.scale_fun_additive [in ssralg]
GRing.scale_fun_head [in ssralg]
GRing.sol [in ssralg]
GRing.subrK [in ssralg]
GRing.subrr [in ssralg]
GRing.sub_fun_linear [in ssralg]
GRing.sub_fun_additive [in ssralg]
GRing.sub_fun_head [in ssralg]
GRing.Theory.addIr [in ssralg]
GRing.Theory.addKr [in ssralg]
GRing.Theory.addNKr [in ssralg]
GRing.Theory.addNr [in ssralg]
GRing.Theory.addrA [in ssralg]
GRing.Theory.addrAC [in ssralg]
GRing.Theory.addrC [in ssralg]
GRing.Theory.addrCA [in ssralg]
GRing.Theory.addrI [in ssralg]
GRing.Theory.addrK [in ssralg]
GRing.Theory.addrN [in ssralg]
GRing.Theory.addrNK [in ssralg]
GRing.Theory.addr_eq0 [in ssralg]
GRing.Theory.addr0 [in ssralg]
GRing.Theory.add0r [in ssralg]
GRing.Theory.bij_linear [in ssralg]
GRing.Theory.bij_additive [in ssralg]
GRing.Theory.bij_rmorphism [in ssralg]
GRing.Theory.bij_lrmorphism [in ssralg]
GRing.Theory.bin_lt_charf_0 [in ssralg]
GRing.Theory.can2_linear [in ssralg]
GRing.Theory.can2_lrmorphism [in ssralg]
GRing.Theory.can2_additive [in ssralg]
GRing.Theory.can2_rmorphism [in ssralg]
GRing.Theory.charf_prime [in ssralg]
GRing.Theory.charf_eq [in ssralg]
GRing.Theory.charf'_nat [in ssralg]
GRing.Theory.charf0 [in ssralg]
GRing.Theory.charf0P [in ssralg]
GRing.Theory.char0_natf_div [in ssralg]
GRing.Theory.commrN1 [in ssralg]
GRing.Theory.commr_nat [in ssralg]
GRing.Theory.commr_muln [in ssralg]
GRing.Theory.commr_inv [in ssralg]
GRing.Theory.commr_unit_mul [in ssralg]
GRing.Theory.commr_exp [in ssralg]
GRing.Theory.commr_sign [in ssralg]
GRing.Theory.commr_sym [in ssralg]
GRing.Theory.commr_opp [in ssralg]
GRing.Theory.commr_add [in ssralg]
GRing.Theory.commr_mul [in ssralg]
GRing.Theory.commr_exp_mull [in ssralg]
GRing.Theory.commr_refl [in ssralg]
GRing.Theory.commr0 [in ssralg]
GRing.Theory.commr1 [in ssralg]
GRing.Theory.divff [in ssralg]
GRing.Theory.divfK [in ssralg]
GRing.Theory.divrK [in ssralg]
GRing.Theory.divrr [in ssralg]
GRing.Theory.divr1 [in ssralg]
GRing.Theory.div1r [in ssralg]
GRing.Theory.dvdn_charf [in ssralg]
GRing.Theory.eqr_opp [in ssralg]
GRing.Theory.eqr_oppC [in ssralg]
GRing.Theory.eq_sol [in ssralg]
GRing.Theory.eq_holds [in ssralg]
GRing.Theory.eq_sat [in ssralg]
GRing.Theory.eq_eval [in ssralg]
GRing.Theory.eval_tsubst [in ssralg]
GRing.Theory.expfS_eq1 [in ssralg]
GRing.Theory.expf_eq0 [in ssralg]
GRing.Theory.expf_neq0 [in ssralg]
GRing.Theory.exprN [in ssralg]
GRing.Theory.exprn_mulr [in ssralg]
GRing.Theory.exprn_subl [in ssralg]
GRing.Theory.exprn_dvd [in ssralg]
GRing.Theory.exprn_mulnl [in ssralg]
GRing.Theory.exprn_mull [in ssralg]
GRing.Theory.exprn_addl_comm [in ssralg]
GRing.Theory.exprn_subl_comm [in ssralg]
GRing.Theory.exprn_addl [in ssralg]
GRing.Theory.exprn_addr [in ssralg]
GRing.Theory.exprn_mod [in ssralg]
GRing.Theory.exprn_add1 [in ssralg]
GRing.Theory.exprS [in ssralg]
GRing.Theory.exprSr [in ssralg]
GRing.Theory.expr_inv [in ssralg]
GRing.Theory.expr0 [in ssralg]
GRing.Theory.expr1 [in ssralg]
GRing.Theory.expr2 [in ssralg]
GRing.Theory.exp1rn [in ssralg]
GRing.Theory.fmorphV [in ssralg]
GRing.Theory.fmorph_eq0 [in ssralg]
GRing.Theory.fmorph_div [in ssralg]
GRing.Theory.fmorph_unit [in ssralg]
GRing.Theory.fmorph_inj [in ssralg]
GRing.Theory.fmorph_char [in ssralg]
GRing.Theory.Frobenius_aut_sub_comm [in ssralg]
GRing.Theory.Frobenius_aut_nat [in ssralg]
GRing.Theory.Frobenius_aut_opp [in ssralg]
GRing.Theory.Frobenius_aut_0 [in ssralg]
GRing.Theory.Frobenius_aut_muln [in ssralg]
GRing.Theory.Frobenius_aut_1 [in ssralg]
GRing.Theory.Frobenius_aut_add_comm [in ssralg]
GRing.Theory.Frobenius_autE [in ssralg]
GRing.Theory.Frobenius_aut_exp [in ssralg]
GRing.Theory.Frobenius_aut_mul_comm [in ssralg]
GRing.Theory.holds_fsubst [in ssralg]
GRing.Theory.invf_mul [in ssralg]
GRing.Theory.invrK [in ssralg]
GRing.Theory.invrN [in ssralg]
GRing.Theory.invr_inj [in ssralg]
GRing.Theory.invr_out [in ssralg]
GRing.Theory.invr_mul [in ssralg]
GRing.Theory.invr_eq0 [in ssralg]
GRing.Theory.invr_neq0 [in ssralg]
GRing.Theory.invr0 [in ssralg]
GRing.Theory.invr1 [in ssralg]
GRing.Theory.linearD [in ssralg]
GRing.Theory.linearMn [in ssralg]
GRing.Theory.linearMNn [in ssralg]
GRing.Theory.linearN [in ssralg]
GRing.Theory.linearP [in ssralg]
GRing.Theory.linearZ [in ssralg]
GRing.Theory.linear_sum [in ssralg]
GRing.Theory.linear_sub [in ssralg]
GRing.Theory.linear0 [in ssralg]
GRing.Theory.mulfI [in ssralg]
GRing.Theory.mulfK [in ssralg]
GRing.Theory.mulfV [in ssralg]
GRing.Theory.mulfVK [in ssralg]
GRing.Theory.mulf_eq0 [in ssralg]
GRing.Theory.mulf_neq0 [in ssralg]
GRing.Theory.mulIf [in ssralg]
GRing.Theory.mulIr [in ssralg]
GRing.Theory.mulKf [in ssralg]
GRing.Theory.mulKr [in ssralg]
GRing.Theory.mulNr [in ssralg]
GRing.Theory.mulNrn [in ssralg]
GRing.Theory.mulN1r [in ssralg]
GRing.Theory.mulrA [in ssralg]
GRing.Theory.mulrAC [in ssralg]
GRing.Theory.mulrb [in ssralg]
GRing.Theory.mulrC [in ssralg]
GRing.Theory.mulrCA [in ssralg]
GRing.Theory.mulrI [in ssralg]
GRing.Theory.mulrK [in ssralg]
GRing.Theory.mulrN [in ssralg]
GRing.Theory.mulrnA [in ssralg]
GRing.Theory.mulrnAC [in ssralg]
GRing.Theory.mulrnAl [in ssralg]
GRing.Theory.mulrnAr [in ssralg]
GRing.Theory.mulrNN [in ssralg]
GRing.Theory.mulrn_addr [in ssralg]
GRing.Theory.mulrn_subr [in ssralg]
GRing.Theory.mulrn_addl [in ssralg]
GRing.Theory.mulrn_subl [in ssralg]
GRing.Theory.mulrN1 [in ssralg]
GRing.Theory.mulrS [in ssralg]
GRing.Theory.mulrSr [in ssralg]
GRing.Theory.mulrV [in ssralg]
GRing.Theory.mulrVK [in ssralg]
GRing.Theory.mulr_addl [in ssralg]
GRing.Theory.mulr_sumr [in ssralg]
GRing.Theory.mulr_natr [in ssralg]
GRing.Theory.mulr_addr [in ssralg]
GRing.Theory.mulr_subl [in ssralg]
GRing.Theory.mulr_suml [in ssralg]
GRing.Theory.mulr_natl [in ssralg]
GRing.Theory.mulr_subr [in ssralg]
GRing.Theory.mulr0 [in ssralg]
GRing.Theory.mulr0n [in ssralg]
GRing.Theory.mulr1 [in ssralg]
GRing.Theory.mulr1n [in ssralg]
GRing.Theory.mulr2n [in ssralg]
GRing.Theory.mulVf [in ssralg]
GRing.Theory.mulVKf [in ssralg]
GRing.Theory.mulVKr [in ssralg]
GRing.Theory.mulVr [in ssralg]
GRing.Theory.mul0r [in ssralg]
GRing.Theory.mul0rn [in ssralg]
GRing.Theory.mul1r [in ssralg]
GRing.Theory.natf0_char [in ssralg]
GRing.Theory.natr_add [in ssralg]
GRing.Theory.natr_sub [in ssralg]
GRing.Theory.natr_sum [in ssralg]
GRing.Theory.natr_mul [in ssralg]
GRing.Theory.natr_exp [in ssralg]
GRing.Theory.natr_div [in ssralg]
GRing.Theory.nonzero1r [in ssralg]
GRing.Theory.oner_eq0 [in ssralg]
GRing.Theory.opprK [in ssralg]
GRing.Theory.oppr_eq0 [in ssralg]
GRing.Theory.oppr_add [in ssralg]
GRing.Theory.oppr_sub [in ssralg]
GRing.Theory.oppr0 [in ssralg]
GRing.Theory.prodf_inv [in ssralg]
GRing.Theory.prodr_opp [in ssralg]
GRing.Theory.prodr_exp_r [in ssralg]
GRing.Theory.prodr_exp [in ssralg]
GRing.Theory.prodr_const [in ssralg]
GRing.Theory.raddfD [in ssralg]
GRing.Theory.raddfMn [in ssralg]
GRing.Theory.raddfMNn [in ssralg]
GRing.Theory.raddfN [in ssralg]
GRing.Theory.raddf_sub [in ssralg]
GRing.Theory.raddf_sum [in ssralg]
GRing.Theory.raddf0 [in ssralg]
GRing.Theory.rmorphD [in ssralg]
GRing.Theory.rmorphismMP [in ssralg]
GRing.Theory.rmorphismP [in ssralg]
GRing.Theory.rmorphM [in ssralg]
GRing.Theory.rmorphMn [in ssralg]
GRing.Theory.rmorphMNn [in ssralg]
GRing.Theory.rmorphN [in ssralg]
GRing.Theory.rmorphV [in ssralg]
GRing.Theory.rmorphX [in ssralg]
GRing.Theory.rmorph_comm [in ssralg]
GRing.Theory.rmorph_prod [in ssralg]
GRing.Theory.rmorph_sum [in ssralg]
GRing.Theory.rmorph_div [in ssralg]
GRing.Theory.rmorph_nat [in ssralg]
GRing.Theory.rmorph_sub [in ssralg]
GRing.Theory.rmorph_char [in ssralg]
GRing.Theory.rmorph_unit [in ssralg]
GRing.Theory.rmorph_sign [in ssralg]
GRing.Theory.rmorph0 [in ssralg]
GRing.Theory.rmorph1 [in ssralg]
GRing.Theory.satP [in ssralg]
GRing.Theory.scaleNr [in ssralg]
GRing.Theory.scaleN1r [in ssralg]
GRing.Theory.scalerA [in ssralg]
GRing.Theory.scalerI [in ssralg]
GRing.Theory.scalerK [in ssralg]
GRing.Theory.scalerKV [in ssralg]
GRing.Theory.scalerN [in ssralg]
GRing.Theory.scaler_injl [in ssralg]
GRing.Theory.scaler_eq0 [in ssralg]
GRing.Theory.scaler_prod [in ssralg]
GRing.Theory.scaler_exp [in ssralg]
GRing.Theory.scaler_sumr [in ssralg]
GRing.Theory.scaler_swap [in ssralg]
GRing.Theory.scaler_suml [in ssralg]
GRing.Theory.scaler_mulr [in ssralg]
GRing.Theory.scaler_mull [in ssralg]
GRing.Theory.scaler_mulrnl [in ssralg]
GRing.Theory.scaler_nat [in ssralg]
GRing.Theory.scaler_addl [in ssralg]
GRing.Theory.scaler_prodl [in ssralg]
GRing.Theory.scaler_mulrnr [in ssralg]
GRing.Theory.scaler_subr [in ssralg]
GRing.Theory.scaler_addr [in ssralg]
GRing.Theory.scaler_inv [in ssralg]
GRing.Theory.scaler_subl [in ssralg]
GRing.Theory.scaler_unit [in ssralg]
GRing.Theory.scaler_prodr [in ssralg]
GRing.Theory.scaler0 [in ssralg]
GRing.Theory.scale0r [in ssralg]
GRing.Theory.scale1r [in ssralg]
GRing.Theory.signr_addb [in ssralg]
GRing.Theory.signr_odd [in ssralg]
GRing.Theory.signr_eq0 [in ssralg]
GRing.Theory.size_sol [in ssralg]
GRing.Theory.solP [in ssralg]
GRing.Theory.solve_monicpoly [in ssralg]
GRing.Theory.sqrf_eq1 [in ssralg]
GRing.Theory.sqrrN [in ssralg]
GRing.Theory.sqrr_add [in ssralg]
GRing.Theory.sqrr_sub [in ssralg]
GRing.Theory.sqrr_add1 [in ssralg]
GRing.Theory.sqrr_sub1 [in ssralg]
GRing.Theory.subrK [in ssralg]
GRing.Theory.subrr [in ssralg]
GRing.Theory.subr_eq [in ssralg]
GRing.Theory.subr_sqr [in ssralg]
GRing.Theory.subr_sqr_add_sub [in ssralg]
GRing.Theory.subr_expn_comm [in ssralg]
GRing.Theory.subr_sqr_1 [in ssralg]
GRing.Theory.subr_expn_1 [in ssralg]
GRing.Theory.subr_expn [in ssralg]
GRing.Theory.subr_eq0 [in ssralg]
GRing.Theory.subr0 [in ssralg]
GRing.Theory.sub0r [in ssralg]
GRing.Theory.sumr_muln [in ssralg]
GRing.Theory.sumr_const [in ssralg]
GRing.Theory.sumr_muln_r [in ssralg]
GRing.Theory.sumr_opp [in ssralg]
GRing.Theory.sumr_sub [in ssralg]
GRing.Theory.unitfE [in ssralg]
GRing.Theory.unitrE [in ssralg]
GRing.Theory.unitrP [in ssralg]
GRing.Theory.unitr_pexp [in ssralg]
GRing.Theory.unitr_inv [in ssralg]
GRing.Theory.unitr_mull [in ssralg]
GRing.Theory.unitr_opp [in ssralg]
GRing.Theory.unitr_exp [in ssralg]
GRing.Theory.unitr_mul [in ssralg]
GRing.Theory.unitr_mulr [in ssralg]
GRing.Theory.unitr0 [in ssralg]
GRing.Theory.unitr1 [in ssralg]
GRing.to_rterm [in ssralg]
GRing.to_rform [in ssralg]
GRing.tsubst [in ssralg]
GRing.ub_var [in ssralg]
GRing.unit [in ssralg]
GRing.UnitAlgebra.algType [in ssralg]
GRing.UnitAlgebra.alg_unitRingType [in ssralg]
GRing.UnitAlgebra.base2 [in ssralg]
GRing.UnitAlgebra.choiceType [in ssralg]
GRing.UnitAlgebra.class [in ssralg]
GRing.UnitAlgebra.eqType [in ssralg]
GRing.UnitAlgebra.lalgType [in ssralg]
GRing.UnitAlgebra.lalg_unitRingType [in ssralg]
GRing.UnitAlgebra.lmodType [in ssralg]
GRing.UnitAlgebra.lmod_unitRingType [in ssralg]
GRing.UnitAlgebra.pack [in ssralg]
GRing.UnitAlgebra.ringType [in ssralg]
GRing.UnitAlgebra.unitRingType [in ssralg]
GRing.UnitAlgebra.zmodType [in ssralg]
GRing.UnitRing.choiceType [in ssralg]
GRing.UnitRing.class [in ssralg]
GRing.UnitRing.clone [in ssralg]
GRing.UnitRing.eqType [in ssralg]
GRing.UnitRing.EtaMixin [in ssralg]
GRing.UnitRing.pack [in ssralg]
GRing.UnitRing.ringType [in ssralg]
GRing.UnitRing.zmodType [in ssralg]
GRing.zero [in ssralg]
GRing.Zmodule.choiceType [in ssralg]
GRing.Zmodule.class [in ssralg]
GRing.Zmodule.clone [in ssralg]
GRing.Zmodule.eqType [in ssralg]
GRing.Zmodule.pack [in ssralg]
group [in fingroup]
groupCl [in mxrepresentation]
GroupSetBaseGroupSig.sort [in fingroup]
GroupSet.sort [in fingroup]
group_of [in fingroup]
group_splitting_field [in mxrepresentation]
group_of_subFinType [in fingroup]
group_of_finType [in fingroup]
group_of_subCountType [in fingroup]
group_of_countType [in fingroup]
group_of_choiceType [in fingroup]
group_of_eqType [in fingroup]
group_of_subType [in fingroup]
group_subFinType [in fingroup]
group_finType [in fingroup]
group_subCountType [in fingroup]
group_countType [in fingroup]
group_choiceType [in fingroup]
group_eqType [in fingroup]
group_subType [in fingroup]
group_set_finType [in fingroup]
group_set_countType [in fingroup]
group_set_choiceType [in fingroup]
group_set_eqType [in fingroup]
group_set_of_baseGroupType [in fingroup]
group_set_baseGroupType [in fingroup]
group_rel_of [in gseries]
group_finMixin [in fingroup]
group_closure_field [in mxrepresentation]
group_countMixin [in fingroup]
group_ring [in mxrepresentation]
group_set_baseGroupMixin [in fingroup]
group_choiceMixin [in fingroup]
group_eqMixin [in fingroup]
group_set [in fingroup]
GrpQ [in extremal]
gset_mx [in mxrepresentation]
gsimp [in fingroup]
gtn [in ssrnat]
gt_ [in center]
gzZ [in center]
gzZchar [in center]
gzZ_lone [in center]
G_ [in center]



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)