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

gacentC [in action]
gacentD1 [in action]
gacentE [in action]
gacentEsd [in gproduct]
gacentIdom [in action]
gacentIim [in action]
gacentJ [in action]
gacentM [in action]
gacentQ [in action]
gacentS [in action]
gacentU [in action]
gacentY [in action]
gacent_repr [in mxabelem]
gacent_ract [in action]
gacent_gen [in action]
gacent_comp [in action]
gacent_cycle [in action]
gacent_mod [in action]
gacent_actby [in action]
gacent1 [in action]
gacent1E [in action]
gactJ [in action]
gactM [in action]
gactR [in action]
gactsI [in jordanholder]
gactsM [in jordanholder]
gactsP [in jordanholder]
gacts_range [in action]
gacts_char [in action]
gactV [in action]
gactX [in action]
gact_stable [in action]
gact_out [in action]
gact1 [in action]
Gaschutz_transitive [in finmodule]
Gaschutz_split [in finmodule]
gastabsP [in jordanholder]
gauss [in div]
gaussian_elimination_map [in mxalgebra]
gauss_gcdl [in div]
gauss_inv [in div]
gauss_gcdr [in div]
gcdnA [in div]
gcdnAC [in div]
gcdnC [in div]
gcdnCA [in div]
gcdnE [in div]
gcdnn [in div]
gcdn_addr [in div]
gcdn_mull [in div]
gcdn_addl [in div]
gcdn_addl_mul [in div]
gcdn_mul2l [in div]
gcdn_mulr [in div]
gcdn_exp [in div]
gcdn_modr [in div]
gcdn_gt0 [in div]
gcdn_modl [in div]
gcdn_def [in div]
gcdn_divnC [in div]
gcdn0 [in div]
gcdn1 [in div]
gcdpC [in poly]
gcdpE [in poly]
gcdpp [in poly]
gcdp_map [in poly]
gcdp0 [in poly]
gcd0n [in div]
gcd0p [in poly]
gcd1n [in div]
gcore_sub [in fingroup]
gcore_max [in fingroup]
gcore_norm [in fingroup]
gcore_normal [in fingroup]
genD [in fingroup]
genDU [in fingroup]
genD1 [in fingroup]
genD1id [in fingroup]
generatedP [in fingroup]
generators_quaternion [in extremal]
generators_semidihedral [in extremal]
generators_modular_group [in extremal]
generators_2dihedral [in extremal]
generator_cycle [in cyclic]
generator_order [in cyclic]
generator_coprime [in cyclic]
genGid [in fingroup]
genGidG [in fingroup]
genJ [in fingroup]
genmxE [in mxalgebra]
genmxP [in mxalgebra]
genmx_key [in mxalgebra]
genmx_id [in mxalgebra]
genmx_adds [in mxalgebra]
genmx_component [in mxrepresentation]
genmx_sums [in mxalgebra]
genmx_bigcap [in mxalgebra]
genmx_muls [in mxalgebra]
genmx_Socle [in mxrepresentation]
genmx_diff [in mxalgebra]
genmx_cap [in mxalgebra]
genmx0 [in mxalgebra]
genmx1 [in mxalgebra]
genM_join [in fingroup]
genS [in fingroup]
genV [in fingroup]
gen_expgs [in fingroup]
gen_prodgP [in fingroup]
gen_subG [in fingroup]
gen_set_id [in fingroup]
gen0 [in fingroup]
geq_leqif [in ssrnat]
gFchar [in gfunctor]
gFcompS [in gfunctor]
gFcomp_closed [in gfunctor]
gFcomp_cont [in gfunctor]
gFcont [in gfunctor]
gFgroupset [in gfunctor]
gFhereditary [in gfunctor]
gFid [in gfunctor]
gFisog [in gfunctor]
gFisom [in gfunctor]
gFiso_cont [in gfunctor]
gFmod_hereditary [in gfunctor]
gFmod_cont [in gfunctor]
gFmod_closed [in gfunctor]
gFnorm [in gfunctor]
gFnormal [in gfunctor]
gFsub [in gfunctor]
gFunctorI [in gfunctor]
gFunctorS [in gfunctor]
GFunctor.continuous_is_iso_continuous [in gfunctor]
GFunctor.pcontinuous_is_continuous [in gfunctor]
GFunctor.pcontinuous_is_hereditary [in gfunctor]
GLmx_faithful [in mxabelem]
GL_MxE [in matrix]
GL_1E [in matrix]
GL_det [in matrix]
GL_VE [in matrix]
GL_ME [in matrix]
GL_unit [in matrix]
GL_VxE [in matrix]
GL_unitmx [in matrix]
GL_mx_repr [in mxabelem]
grank_min [in abelian]
grank_abelian [in abelian]
grank_witness [in abelian]
gring_valK [in mxrepresentation]
gring_rowK [in mxrepresentation]
gring_row_mul [in mxrepresentation]
gring_op_mx [in mxrepresentation]
gring_op1 [in mxrepresentation]
gring_opM [in mxrepresentation]
gring_mxP [in mxrepresentation]
gring_free [in mxrepresentation]
gring_indexK [in mxrepresentation]
gring_opG [in mxrepresentation]
gring_mxK [in mxrepresentation]
gring_mxA [in mxrepresentation]
gring_op_id [in mxrepresentation]
gring_mxJ [in mxrepresentation]
gring_opJ [in mxrepresentation]
gring_projE [in mxrepresentation]
gring_opE [in mxrepresentation]
GRing.addIr [in ssralg]
GRing.addKr [in ssralg]
GRing.addNKr [in ssralg]
GRing.addNr [in ssralg]
GRing.addrA [in ssralg]
GRing.addrAC [in ssralg]
GRing.addrC [in ssralg]
GRing.addrCA [in ssralg]
GRing.addrI [in ssralg]
GRing.addrK [in ssralg]
GRing.addrN [in ssralg]
GRing.addrNK [in ssralg]
GRing.addr_eq0 [in ssralg]
GRing.addr0 [in ssralg]
GRing.add_fun_is_scalable [in ssralg]
GRing.add_fun_is_additive [in ssralg]
GRing.add0r [in ssralg]
GRing.Algebra.comm_axiom [in ssralg]
GRing.and_dnfP [in ssralg]
GRing.bij_lrmorphism [in ssralg]
GRing.bij_linear [in ssralg]
GRing.bij_rmorphism [in ssralg]
GRing.bij_additive [in ssralg]
GRing.bin_lt_charf_0 [in ssralg]
GRing.can2_lrmorphism [in ssralg]
GRing.can2_additive [in ssralg]
GRing.can2_rmorphism [in ssralg]
GRing.can2_linear [in ssralg]
GRing.cat_dnfP [in ssralg]
GRing.charf_prime [in ssralg]
GRing.charf_eq [in ssralg]
GRing.charf'_nat [in ssralg]
GRing.charf0 [in ssralg]
GRing.charf0P [in ssralg]
GRing.char0_natf_div [in ssralg]
GRing.commrN1 [in ssralg]
GRing.commr_nat [in ssralg]
GRing.commr_refl [in ssralg]
GRing.commr_exp [in ssralg]
GRing.commr_opp [in ssralg]
GRing.commr_muln [in ssralg]
GRing.commr_mul [in ssralg]
GRing.commr_unit_mul [in ssralg]
GRing.commr_inv [in ssralg]
GRing.commr_sign [in ssralg]
GRing.commr_exp_mull [in ssralg]
GRing.commr_add [in ssralg]
GRing.commr_sym [in ssralg]
GRing.commr0 [in ssralg]
GRing.commr1 [in ssralg]
GRing.comp_is_additive [in ssralg]
GRing.comp_is_scalable [in ssralg]
GRing.ComUnitRing.mulC_unitP [in ssralg]
GRing.ComUnitRing.mulC_mulrV [in ssralg]
GRing.divff [in ssralg]
GRing.divrr [in ssralg]
GRing.divr1 [in ssralg]
GRing.div1r [in ssralg]
GRing.dnf_to_form_qf [in ssralg]
GRing.dnf_to_rform [in ssralg]
GRing.dvdn_charf [in ssralg]
GRing.eqr_opp [in ssralg]
GRing.eqr_oppC [in ssralg]
GRing.eq_eval [in ssralg]
GRing.eq_sat [in ssralg]
GRing.eq_sol [in ssralg]
GRing.eq_holds [in ssralg]
GRing.eval_Pick [in ssralg]
GRing.eval_tsubst [in ssralg]
GRing.expfS_eq1 [in ssralg]
GRing.expf_neq0 [in ssralg]
GRing.expf_eq0 [in ssralg]
GRing.exprN [in ssralg]
GRing.exprn_addr [in ssralg]
GRing.exprn_subl_comm [in ssralg]
GRing.exprn_mod [in ssralg]
GRing.exprn_subl [in ssralg]
GRing.exprn_addl_comm [in ssralg]
GRing.exprn_addl [in ssralg]
GRing.exprn_dvd [in ssralg]
GRing.exprn_mulr [in ssralg]
GRing.exprn_mull [in ssralg]
GRing.exprn_add1 [in ssralg]
GRing.exprn_mulnl [in ssralg]
GRing.exprS [in ssralg]
GRing.exprSr [in ssralg]
GRing.expr_inv [in ssralg]
GRing.expr0 [in ssralg]
GRing.expr1 [in ssralg]
GRing.expr2 [in ssralg]
GRing.exp1rn [in ssralg]
GRing.Field.IdomainMixin [in ssralg]
GRing.Field.intro_unit [in ssralg]
GRing.Field.inv_out [in ssralg]
GRing.Field.Mixin [in ssralg]
GRing.fmorphV [in ssralg]
GRing.fmorph_eq0 [in ssralg]
GRing.fmorph_char [in ssralg]
GRing.fmorph_inj [in ssralg]
GRing.fmorph_div [in ssralg]
GRing.fmorph_unit [in ssralg]
GRing.foldExistsP [in ssralg]
GRing.foldForallP [in ssralg]
GRing.Frobenius_aut_0 [in ssralg]
GRing.Frobenius_aut_is_rmorphism [in ssralg]
GRing.Frobenius_aut_1 [in ssralg]
GRing.Frobenius_aut_muln [in ssralg]
GRing.Frobenius_aut_mul_comm [in ssralg]
GRing.Frobenius_aut_sub_comm [in ssralg]
GRing.Frobenius_aut_exp [in ssralg]
GRing.Frobenius_aut_add_comm [in ssralg]
GRing.Frobenius_aut_nat [in ssralg]
GRing.Frobenius_autE [in ssralg]
GRing.Frobenius_aut_opp [in ssralg]
GRing.holds_fsubst [in ssralg]
GRing.holds_proj [in ssralg]
GRing.idfun_is_multiplicative [in ssralg]
GRing.idfun_is_scalable [in ssralg]
GRing.idfun_is_additive [in ssralg]
GRing.invf_mul [in ssralg]
GRing.invrK [in ssralg]
GRing.invrN [in ssralg]
GRing.invr_neq0 [in ssralg]
GRing.invr_eq0 [in ssralg]
GRing.invr_mul [in ssralg]
GRing.invr_inj [in ssralg]
GRing.invr_out [in ssralg]
GRing.invr0 [in ssralg]
GRing.invr1 [in ssralg]
GRing.in_alg_is_rmorphism [in ssralg]
GRing.linearD [in ssralg]
GRing.linearMn [in ssralg]
GRing.linearMNn [in ssralg]
GRing.linearN [in ssralg]
GRing.linearP [in ssralg]
GRing.linearZ [in ssralg]
GRing.linear_sub [in ssralg]
GRing.linear_sum [in ssralg]
GRing.Linear.class_of_axiom [in ssralg]
GRing.linear0 [in ssralg]
GRing.mulfI [in ssralg]
GRing.mulfK [in ssralg]
GRing.mulfVK [in ssralg]
GRing.mulf_eq0 [in ssralg]
GRing.mulf_neq0 [in ssralg]
GRing.mulIf [in ssralg]
GRing.mulIr [in ssralg]
GRing.mulKf [in ssralg]
GRing.mulKr [in ssralg]
GRing.mull_fun_is_additive [in ssralg]
GRing.mull_fun_is_scalable [in ssralg]
GRing.mulNr [in ssralg]
GRing.mulNrn [in ssralg]
GRing.mulN1r [in ssralg]
GRing.mulrA [in ssralg]
GRing.mulrAC [in ssralg]
GRing.mulrb [in ssralg]
GRing.mulrC [in ssralg]
GRing.mulrCA [in ssralg]
GRing.mulrI [in ssralg]
GRing.mulrK [in ssralg]
GRing.mulrN [in ssralg]
GRing.mulrnA [in ssralg]
GRing.mulrnAC [in ssralg]
GRing.mulrnAl [in ssralg]
GRing.mulrnAr [in ssralg]
GRing.mulrNN [in ssralg]
GRing.mulrn_subr [in ssralg]
GRing.mulrn_addr [in ssralg]
GRing.mulrn_subl [in ssralg]
GRing.mulrn_addl [in ssralg]
GRing.mulrN1 [in ssralg]
GRing.mulrS [in ssralg]
GRing.mulrSr [in ssralg]
GRing.mulrVK [in ssralg]
GRing.mulr_fun_is_scalable [in ssralg]
GRing.mulr_addl [in ssralg]
GRing.mulr_fun_is_additive [in ssralg]
GRing.mulr_addr [in ssralg]
GRing.mulr_natr [in ssralg]
GRing.mulr_suml [in ssralg]
GRing.mulr_subl [in ssralg]
GRing.mulr_sumr [in ssralg]
GRing.mulr_subr [in ssralg]
GRing.mulr_natl [in ssralg]
GRing.mulr0 [in ssralg]
GRing.mulr0n [in ssralg]
GRing.mulr1 [in ssralg]
GRing.mulr1n [in ssralg]
GRing.mulr2n [in ssralg]
GRing.mulVf [in ssralg]
GRing.mulVKf [in ssralg]
GRing.mulVKr [in ssralg]
GRing.mulVr [in ssralg]
GRing.mul0r [in ssralg]
GRing.mul0rn [in ssralg]
GRing.mul1r [in ssralg]
GRing.natf0_char [in ssralg]
GRing.natr_sub [in ssralg]
GRing.natr_exp [in ssralg]
GRing.natr_div [in ssralg]
GRing.natr_add [in ssralg]
GRing.natr_mul [in ssralg]
GRing.nonzero1r [in ssralg]
GRing.null_fun_is_scalable [in ssralg]
GRing.null_fun_is_additive [in ssralg]
GRing.oner_eq0 [in ssralg]
GRing.opprK [in ssralg]
GRing.oppr_add [in ssralg]
GRing.oppr_sub [in ssralg]
GRing.oppr_eq0 [in ssralg]
GRing.oppr0 [in ssralg]
GRing.opp_is_scalable [in ssralg]
GRing.opp_is_additive [in ssralg]
GRing.Pick_form_qf [in ssralg]
GRing.prodf_inv [in ssralg]
GRing.prodr_exp_r [in ssralg]
GRing.prodr_exp [in ssralg]
GRing.prodr_opp [in ssralg]
GRing.prodr_const [in ssralg]
GRing.proj_satP [in ssralg]
GRing.qf_to_dnfP [in ssralg]
GRing.qf_evalP [in ssralg]
GRing.qf_to_dnf_rterm [in ssralg]
GRing.quantifier_elim_wf [in ssralg]
GRing.quantifier_elim_rformP [in ssralg]
GRing.raddfD [in ssralg]
GRing.raddfMn [in ssralg]
GRing.raddfMNn [in ssralg]
GRing.raddfN [in ssralg]
GRing.raddf_sub [in ssralg]
GRing.raddf_sum [in ssralg]
GRing.raddf0 [in ssralg]
GRing.rev_unitrP [in ssralg]
GRing.rmorphD [in ssralg]
GRing.rmorphismMP [in ssralg]
GRing.rmorphismP [in ssralg]
GRing.rmorphM [in ssralg]
GRing.rmorphMn [in ssralg]
GRing.rmorphMNn [in ssralg]
GRing.rmorphN [in ssralg]
GRing.rmorphV [in ssralg]
GRing.rmorphX [in ssralg]
GRing.rmorph_sub [in ssralg]
GRing.rmorph_comm [in ssralg]
GRing.rmorph_unit [in ssralg]
GRing.rmorph_prod [in ssralg]
GRing.rmorph_nat [in ssralg]
GRing.rmorph_sign [in ssralg]
GRing.rmorph_sum [in ssralg]
GRing.rmorph_div [in ssralg]
GRing.rmorph_char [in ssralg]
GRing.rmorph0 [in ssralg]
GRing.rmorph1 [in ssralg]
GRing.same_env_sym [in ssralg]
GRing.satP [in ssralg]
GRing.scaleNr [in ssralg]
GRing.scaleN1r [in ssralg]
GRing.scalerA [in ssralg]
GRing.scalerI [in ssralg]
GRing.scalerK [in ssralg]
GRing.scalerKV [in ssralg]
GRing.scalerN [in ssralg]
GRing.scaler_subr [in ssralg]
GRing.scaler_unit [in ssralg]
GRing.scaler_swap [in ssralg]
GRing.scaler_inv [in ssralg]
GRing.scaler_prod [in ssralg]
GRing.scaler_mulr [in ssralg]
GRing.scaler_subl [in ssralg]
GRing.scaler_eq0 [in ssralg]
GRing.scaler_sumr [in ssralg]
GRing.scaler_exp [in ssralg]
GRing.scaler_injl [in ssralg]
GRing.scaler_addl [in ssralg]
GRing.scaler_prodl [in ssralg]
GRing.scaler_prodr [in ssralg]
GRing.scaler_mull [in ssralg]
GRing.scaler_mulrnl [in ssralg]
GRing.scaler_mulrnr [in ssralg]
GRing.scaler_addr [in ssralg]
GRing.scaler_nat [in ssralg]
GRing.scaler_suml [in ssralg]
GRing.scaler0 [in ssralg]
GRing.scale_is_scalable [in ssralg]
GRing.scale_is_additive [in ssralg]
GRing.scale_fun_is_additive [in ssralg]
GRing.scale_fun_is_scalable [in ssralg]
GRing.scale0r [in ssralg]
GRing.scale1r [in ssralg]
GRing.signr_eq0 [in ssralg]
GRing.signr_odd [in ssralg]
GRing.signr_addb [in ssralg]
GRing.size_sol [in ssralg]
GRing.solP [in ssralg]
GRing.solve_monicpoly [in ssralg]
GRing.sol_subproof [in ssralg]
GRing.sqrf_eq1 [in ssralg]
GRing.sqrrN [in ssralg]
GRing.sqrr_sub1 [in ssralg]
GRing.sqrr_add [in ssralg]
GRing.sqrr_sub [in ssralg]
GRing.sqrr_add1 [in ssralg]
GRing.subr_eq [in ssralg]
GRing.subr_sqr [in ssralg]
GRing.subr_sqr_1 [in ssralg]
GRing.subr_eq0 [in ssralg]
GRing.subr_sqr_add_sub [in ssralg]
GRing.subr_expn [in ssralg]
GRing.subr_expn_comm [in ssralg]
GRing.subr_expn_1 [in ssralg]
GRing.subr0 [in ssralg]
GRing.sub_fun_is_scalable [in ssralg]
GRing.sub_fun_is_additive [in ssralg]
GRing.sub0r [in ssralg]
GRing.sumr_opp [in ssralg]
GRing.sumr_muln [in ssralg]
GRing.sumr_muln_r [in ssralg]
GRing.sumr_const [in ssralg]
GRing.sumr_sub [in ssralg]
GRing.to_rform_rformula [in ssralg]
GRing.to_rterm_id [in ssralg]
GRing.to_rformP [in ssralg]
GRing.unitfE [in ssralg]
GRing.unitrE [in ssralg]
GRing.unitrP [in ssralg]
GRing.unitr_mul [in ssralg]
GRing.unitr_opp [in ssralg]
GRing.unitr_pexp [in ssralg]
GRing.unitr_exp [in ssralg]
GRing.unitr_mulr [in ssralg]
GRing.unitr_mull [in ssralg]
GRing.unitr_inv [in ssralg]
GRing.unitr0 [in ssralg]
GRing.unitr1 [in ssralg]
GRing.wf_proj [in ssralg]
groupD1_inj [in fingroup]
groupJ [in fingroup]
groupJr [in fingroup]
groupM [in fingroup]
groupMl [in fingroup]
groupMr [in fingroup]
groupP [in fingroup]
groupR [in fingroup]
groupV [in fingroup]
groupVl [in fingroup]
groupVr [in fingroup]
groupX [in fingroup]
group_closure_field_exists [in mxrepresentation]
group_setT [in fingroup]
group_setP [in fingroup]
group_set_gacent [in action]
group_set_astab [in action]
group_setX [in gproduct]
group_set_astabs [in action]
group_not0 [in gproduct]
group_set_conjG [in fingroup]
group_splitting_field_exists [in mxrepresentation]
group_modl [in fingroup]
group_set_normaliser [in fingroup]
group_Ldiv [in abelian]
group_set_one [in fingroup]
group_prod [in fingroup]
group_setI [in fingroup]
group_modr [in fingroup]
group_inj [in fingroup]
group_set_bigcap [in fingroup]
group0 [in gproduct]
group1 [in fingroup]
group1_class12 [in fingroup]
group1_finType [in fingroup]
group1_contra [in fingroup]
group1_class2 [in fingroup]
group1_class1 [in fingroup]
group1_eqType [in fingroup]
Grp_dihedral [in extremal]
Grp_quaternion [in extremal]
Grp_modular_group [in extremal]
Grp_2dihedral [in extremal]
Grp_ext_dihedral [in extremal]
Grp_pX1p2 [in extraspecial]
Grp_semidihedral [in extremal]
Grp'_dihedral [in extremal]
gtnNdvd [in div]



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)