G (Lemmas)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
G (Lemmas)
gacent1 [prf, in mathcomp.finite_group.action]gacent1E [prf, in mathcomp.finite_group.action]
gacent_actby [prf, in mathcomp.finite_group.action]
gacent_comp [prf, in mathcomp.finite_group.action]
gacent_cycle [prf, in mathcomp.finite_group.action]
gacent_gen [prf, in mathcomp.finite_group.action]
gacent_mod [prf, in mathcomp.finite_group.action]
gacent_ract [prf, in mathcomp.finite_group.action]
gacent_repr [prf, in mathcomp.group_representation.mxabelem]
gacentC [prf, in mathcomp.finite_group.action]
gacentD1 [prf, in mathcomp.finite_group.action]
gacentE [prf, in mathcomp.finite_group.action]
gacentEsd [prf, in mathcomp.finite_group.gproduct]
gacentIdom [prf, in mathcomp.finite_group.action]
gacentIim [prf, in mathcomp.finite_group.action]
gacentJ [prf, in mathcomp.finite_group.action]
gacentM [prf, in mathcomp.finite_group.action]
gacentQ [prf, in mathcomp.finite_group.action]
gacentS [prf, in mathcomp.finite_group.action]
gacentU [prf, in mathcomp.finite_group.action]
gacentY [prf, in mathcomp.finite_group.action]
gact1 [prf, in mathcomp.finite_group.action]
gact_out [prf, in mathcomp.finite_group.action]
gact_stable [prf, in mathcomp.finite_group.action]
gactJ [prf, in mathcomp.finite_group.action]
gactM [prf, in mathcomp.finite_group.action]
gactR [prf, in mathcomp.finite_group.action]
gacts_char [prf, in mathcomp.finite_group.action]
gacts_range [prf, in mathcomp.finite_group.action]
gactsI [prf, in mathcomp.solvable.jordanholder]
gactsM [prf, in mathcomp.solvable.jordanholder]
gactsP [prf, in mathcomp.solvable.jordanholder]
gactV [prf, in mathcomp.finite_group.action]
gactX [prf, in mathcomp.finite_group.action]
gal_adjoin_eq [prf, in mathcomp.field.galois]
gal_AEnd [prf, in mathcomp.field.galois]
gal_cap [prf, in mathcomp.field.galois]
gal_conjg [prf, in mathcomp.field.galois]
gal_eqP [prf, in mathcomp.field.galois]
gal_fixedField [prf, in mathcomp.field.galois]
gal_generated [prf, in mathcomp.field.galois]
gal_id [prf, in mathcomp.field.galois]
gal_independent [prf, in mathcomp.field.galois]
gal_independent_contra [prf, in mathcomp.field.galois]
gal_invP [prf, in mathcomp.field.galois]
gal_is_morphism [prf, in mathcomp.field.galois]
gal_kAut [prf, in mathcomp.field.galois]
gal_kHom [prf, in mathcomp.field.galois]
gal_matrix [prf, in mathcomp.field.galois]
gal_mulP [prf, in mathcomp.field.galois]
gal_oneP [prf, in mathcomp.field.galois]
gal_repr_inj [prf, in mathcomp.field.galois]
gal_reprK [prf, in mathcomp.field.galois]
gal_sgvalK [prf, in mathcomp.field.galois]
galK [prf, in mathcomp.field.galois]
galLgen [prf, in mathcomp.field.finfield]
galM [prf, in mathcomp.field.galois]
galNorm0 [prf, in mathcomp.field.galois]
galNorm1 [prf, in mathcomp.field.galois]
galNorm_eq0 [prf, in mathcomp.field.galois]
galNorm_fixedField [prf, in mathcomp.field.galois]
galNorm_gal [prf, in mathcomp.field.galois]
galNorm_prod [prf, in mathcomp.field.galois]
galNormM [prf, in mathcomp.field.galois]
galNormV [prf, in mathcomp.field.galois]
galNormX [prf, in mathcomp.field.galois]
galois_connection [prf, in mathcomp.field.galois]
galois_connection_subset [prf, in mathcomp.field.galois]
galois_connection_subv [prf, in mathcomp.field.galois]
galois_dim [prf, in mathcomp.field.galois]
galois_factors [prf, in mathcomp.field.galois]
galois_fixedField [prf, in mathcomp.field.galois]
galoisS [prf, in mathcomp.field.galois]
galS [prf, in mathcomp.field.galois]
galTrace_fixedField [prf, in mathcomp.field.galois]
galTrace_gal [prf, in mathcomp.field.galois]
galTrace_is_zmod_morphism [prf, in mathcomp.field.galois]
galV [prf, in mathcomp.field.galois]
Gaschutz_split [prf, in mathcomp.solvable.finmodule]
Gaschutz_transitive [prf, in mathcomp.solvable.finmodule]
gastabsP [prf, in mathcomp.solvable.jordanholder]
Gauss_dvd [prf, in mathcomp.boot.div]
Gauss_dvdl [prf, in mathcomp.boot.div]
Gauss_dvdr [prf, in mathcomp.boot.div]
Gauss_dvdz [prf, in mathcomp.algebra.intdiv]
Gauss_dvdzl [prf, in mathcomp.algebra.intdiv]
Gauss_dvdzr [prf, in mathcomp.algebra.intdiv]
Gauss_gcdl [prf, in mathcomp.boot.div]
Gauss_gcdr [prf, in mathcomp.boot.div]
Gauss_gcdzl [prf, in mathcomp.algebra.intdiv]
Gauss_gcdzr [prf, in mathcomp.algebra.intdiv]
Gaussian_elimination_map [prf, in mathcomp.algebra.mxalgebra]
gcd0n [prf, in mathcomp.boot.div]
gcd0z [prf, in mathcomp.algebra.intdiv]
gcd1n [prf, in mathcomp.boot.div]
gcd1z [prf, in mathcomp.algebra.intdiv]
gcdn0 [prf, in mathcomp.boot.div]
gcdn1 [prf, in mathcomp.boot.div]
gcdn_def [prf, in mathcomp.boot.div]
gcdn_gt0 [prf, in mathcomp.boot.div]
gcdn_idPl [prf, in mathcomp.boot.div]
gcdn_idPr [prf, in mathcomp.boot.div]
gcdn_modl [prf, in mathcomp.boot.div]
gcdn_modr [prf, in mathcomp.boot.div]
gcdnA [prf, in mathcomp.boot.div]
gcdnAC [prf, in mathcomp.boot.div]
gcdnACA [prf, in mathcomp.boot.div]
gcdnC [prf, in mathcomp.boot.div]
gcdnCA [prf, in mathcomp.boot.div]
gcdnDl [prf, in mathcomp.boot.div]
gcdnDr [prf, in mathcomp.boot.div]
gcdnE [prf, in mathcomp.boot.div]
gcdnMDl [prf, in mathcomp.boot.div]
gcdnMl [prf, in mathcomp.boot.div]
gcdnMr [prf, in mathcomp.boot.div]
gcdnn [prf, in mathcomp.boot.div]
gcdNz [prf, in mathcomp.algebra.intdiv]
gcdp_polyOver [prf, in mathcomp.field.fieldext]
gcdz0 [prf, in mathcomp.algebra.intdiv]
gcdz1 [prf, in mathcomp.algebra.intdiv]
gcdz_eq0 [prf, in mathcomp.algebra.intdiv]
gcdz_idPl [prf, in mathcomp.algebra.intdiv]
gcdz_idPr [prf, in mathcomp.algebra.intdiv]
gcdz_modl [prf, in mathcomp.algebra.intdiv]
gcdz_modr [prf, in mathcomp.algebra.intdiv]
gcdzA [prf, in mathcomp.algebra.intdiv]
gcdzAC [prf, in mathcomp.algebra.intdiv]
gcdzACA [prf, in mathcomp.algebra.intdiv]
gcdzC [prf, in mathcomp.algebra.intdiv]
gcdzCA [prf, in mathcomp.algebra.intdiv]
gcdzDl [prf, in mathcomp.algebra.intdiv]
gcdzDr [prf, in mathcomp.algebra.intdiv]
gcdzMDl [prf, in mathcomp.algebra.intdiv]
gcdzMl [prf, in mathcomp.algebra.intdiv]
gcdzMr [prf, in mathcomp.algebra.intdiv]
gcdzN [prf, in mathcomp.algebra.intdiv]
gcdzz [prf, in mathcomp.algebra.intdiv]
gcore_max [prf, in mathcomp.finite_group.fingroup]
gcore_norm [prf, in mathcomp.finite_group.fingroup]
gcore_normal [prf, in mathcomp.finite_group.fingroup]
gcore_sub [prf, in mathcomp.finite_group.fingroup]
ge0 [prf, in mathcomp.algebra.interval_inference]
ge0F [prf, in mathcomp.algebra.interval_inference]
ge1F [prf, in mathcomp.algebra.interval_inference]
ge_pinfty [prf, in mathcomp.algebra.interval]
ge_rat0 [prf, in mathcomp.algebra.rat]
ge_rat0_norm [prf, in mathcomp.algebra.rat]
geigenspaceE [prf, in mathcomp.algebra.mxpoly]
gen0 [prf, in mathcomp.finite_group.fingroup]
gen_diso3 [prf, in mathcomp.solvable.burnside_app]
gen_expgs [prf, in mathcomp.finite_group.fingroup]
gen_prodgP [prf, in mathcomp.finite_group.fingroup]
gen_set_id [prf, in mathcomp.finite_group.fingroup]
gen_subG [prf, in mathcomp.finite_group.fingroup]
gen_tperm [prf, in mathcomp.finite_group.perm]
gen_tperm_circular_shift [prf, in mathcomp.solvable.alt]
gen_tperm_step [prf, in mathcomp.algebra.zmodp]
gen_tpermn_circular_shift [prf, in mathcomp.algebra.zmodp]
genD [prf, in mathcomp.finite_group.fingroup]
genD1 [prf, in mathcomp.finite_group.fingroup]
genD1id [prf, in mathcomp.finite_group.fingroup]
genDU [prf, in mathcomp.finite_group.fingroup]
generalized_orthogonality_relation [prf, in mathcomp.group_representation.character]
generatedP [prf, in mathcomp.finite_group.fingroup]
generator_coprime [prf, in mathcomp.solvable.cyclic]
generator_cycle [prf, in mathcomp.solvable.cyclic]
generator_order [prf, in mathcomp.solvable.cyclic]
generators_2dihedral [prf, in mathcomp.solvable.extremal]
generators_modular_group [prf, in mathcomp.solvable.extremal]
generators_quaternion [prf, in mathcomp.solvable.extremal]
generators_semidihedral [prf, in mathcomp.solvable.extremal]
genGid [prf, in mathcomp.finite_group.fingroup]
genGidG [prf, in mathcomp.finite_group.fingroup]
genJ [prf, in mathcomp.finite_group.fingroup]
genM_join [prf, in mathcomp.finite_group.fingroup]
genmx0 [prf, in mathcomp.algebra.mxalgebra]
genmx1 [prf, in mathcomp.algebra.mxalgebra]
genmx_adds [prf, in mathcomp.algebra.mxalgebra]
genmx_bigcap [prf, in mathcomp.algebra.mxalgebra]
genmx_cap [prf, in mathcomp.algebra.mxalgebra]
genmx_component [prf, in mathcomp.group_representation.mxrepresentation]
genmx_diff [prf, in mathcomp.algebra.mxalgebra]
genmx_id [prf, in mathcomp.algebra.mxalgebra]
genmx_muls [prf, in mathcomp.algebra.mxalgebra]
genmx_ortho [prf, in mathcomp.algebra.sesquilinear]
genmx_Socle [prf, in mathcomp.group_representation.mxrepresentation]
genmx_sums [prf, in mathcomp.algebra.mxalgebra]
genmxE [prf, in mathcomp.algebra.mxalgebra]
genmxP [prf, in mathcomp.algebra.mxalgebra]
genS [prf, in mathcomp.finite_group.fingroup]
GenTree.codeK [prf, in mathcomp.boot.choice]
genV [prf, in mathcomp.finite_group.fingroup]
geq_divBl [prf, in mathcomp.boot.div]
geq_half_double [prf, in mathcomp.boot.ssrnat]
geq_leqif [prf, in mathcomp.boot.ssrnat]
geq_max [prf, in mathcomp.boot.ssrnat]
geq_min [prf, in mathcomp.boot.ssrnat]
geq_minl [prf, in mathcomp.boot.ssrnat]
geq_minr [prf, in mathcomp.boot.ssrnat]
geq_uphalf_double [prf, in mathcomp.boot.ssrnat]
getCratK [prf, in mathcomp.field.algC]
gez0_abs [prf, in mathcomp.algebra.ssrint]
gF1 [prf, in mathcomp.solvable.gfunctor]
gFchar [prf, in mathcomp.solvable.gfunctor]
gFchar_trans [prf, in mathcomp.solvable.gfunctor]
gFcomp_closed [prf, in mathcomp.solvable.gfunctor]
gFcomp_cont [prf, in mathcomp.solvable.gfunctor]
gFcompS [prf, in mathcomp.solvable.gfunctor]
gFcont [prf, in mathcomp.solvable.gfunctor]
gFgroupset [prf, in mathcomp.solvable.gfunctor]
gFhereditary [prf, in mathcomp.solvable.gfunctor]
gFid [prf, in mathcomp.solvable.gfunctor]
gFiso_cont [prf, in mathcomp.solvable.gfunctor]
gFisog [prf, in mathcomp.solvable.gfunctor]
gFisom [prf, in mathcomp.solvable.gfunctor]
gFmod_closed [prf, in mathcomp.solvable.gfunctor]
gFmod_cont [prf, in mathcomp.solvable.gfunctor]
gFmod_hereditary [prf, in mathcomp.solvable.gfunctor]
gFnorm [prf, in mathcomp.solvable.gfunctor]
gFnorm_trans [prf, in mathcomp.solvable.gfunctor]
gFnormal [prf, in mathcomp.solvable.gfunctor]
gFnormal_trans [prf, in mathcomp.solvable.gfunctor]
gFnorms [prf, in mathcomp.solvable.gfunctor]
gFsub [prf, in mathcomp.solvable.gfunctor]
gFsub_trans [prf, in mathcomp.solvable.gfunctor]
GFunctor.continuous_is_iso_continuous [prf, in mathcomp.solvable.gfunctor]
GFunctor.pcontinuous_is_continuous [prf, in mathcomp.solvable.gfunctor]
GFunctor.pcontinuous_is_hereditary [prf, in mathcomp.solvable.gfunctor]
gFunctorI [prf, in mathcomp.solvable.gfunctor]
gFunctorS [prf, in mathcomp.solvable.gfunctor]
GL_1E [prf, in mathcomp.algebra.matrix]
GL_det [prf, in mathcomp.algebra.matrix]
GL_ME [prf, in mathcomp.algebra.matrix]
GL_mx_repr [prf, in mathcomp.group_representation.mxabelem]
GL_MxE [prf, in mathcomp.algebra.matrix]
GL_unit [prf, in mathcomp.algebra.matrix]
GL_unitmx [prf, in mathcomp.algebra.matrix]
GL_VE [prf, in mathcomp.algebra.matrix]
GL_VxE [prf, in mathcomp.algebra.matrix]
GLmx_faithful [prf, in mathcomp.group_representation.mxabelem]
gmulf_commute [prf, in mathcomp.boot.monoid]
gmulf_eq1 [prf, in mathcomp.boot.monoid]
gmulf_inj [prf, in mathcomp.boot.monoid]
gmulf_prod [prf, in mathcomp.boot.monoid]
gmulfF [prf, in mathcomp.boot.monoid]
gmulfJ [prf, in mathcomp.boot.monoid]
gmulfR [prf, in mathcomp.boot.monoid]
gmulfV [prf, in mathcomp.boot.monoid]
gmulfXn [prf, in mathcomp.boot.monoid]
gmulfXVn [prf, in mathcomp.boot.monoid]
gpred_prod [prf, in mathcomp.boot.monoid]
gpredF [prf, in mathcomp.boot.monoid]
gpredFC [prf, in mathcomp.boot.monoid]
gpredFl [prf, in mathcomp.boot.monoid]
gpredFr [prf, in mathcomp.boot.monoid]
gpredJ [prf, in mathcomp.boot.monoid]
gpredMl [prf, in mathcomp.boot.monoid]
gpredMr [prf, in mathcomp.boot.monoid]
gpredR [prf, in mathcomp.boot.monoid]
gpredV [prf, in mathcomp.boot.monoid]
gpredXn [prf, in mathcomp.boot.monoid]
gpredXNn [prf, in mathcomp.boot.monoid]
grank_abelian [prf, in mathcomp.solvable.abelian]
grank_min [prf, in mathcomp.solvable.abelian]
grank_witness [prf, in mathcomp.solvable.abelian]
GRing.add_fun_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.addf_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.addKr_pchar2 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.addrK_pchar2 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.addrr_pchar2 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.algMixin [prf, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.and_dnfP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.bin_lt_pcharf_0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_103.intro_unit [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_103.inv_out [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_142.scale0r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_147.addNr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_158.divrr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_158.invr_out [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_158.mulVr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_158.unitrP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_17.mulC_mulrV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_17.mulC_unitP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_174.id [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_179.fieldP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.Builders_374.mulr0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_40.mul0r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_40.mulr0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_414.scalarAr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_626.mul0r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_626.mul1r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_626.mulr0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_626.mulr1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_626.mulrA [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_626.mulrDl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_626.mulrDr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_626.valM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_638.oner_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_651.mulrC [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_663.scale0r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_663.scale1r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_663.scalerA' [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_663.scalerDl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_663.scalerDr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_663.valZ [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_675.scalerAl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Builders_685.scalerAr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.can2_linear [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.can2_monoid_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.can2_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.can2_semilinear [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.cat_dnfP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.comm_alg [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commr0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commr1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commr_nat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commr_prod [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commr_refl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commr_sign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commr_sum [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commr_sym [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commrB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commrD [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commrM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commrMn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commrN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commrN1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.commrV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.commrX [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.comp_is_monoid_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.comp_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.comRingMixin [prf, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.div1r [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divalg_closedBdiv [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divalg_closedZ [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divff [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divfI [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divIf [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divIr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divKf [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divKr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divr1 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divr1_eq [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divr_closedM [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divr_closedV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divr_signM [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divrI [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divring_closed_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divring_closedBM [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divringClosedP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divrN [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divrNN [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.divrr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.dnf_to_form_qf [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.dnf_to_rform [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.dvdn_pcharf [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.eq_eval [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.eq_holds [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.eq_sat [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.eq_sol [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.eqf_sqr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.eqr_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.eqr_sum_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.eval_If [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.eval_Pick [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.eval_tsubst [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.expf_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.expf_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.expfB [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.expfB_cond [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.expfS_eq1 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.expr0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.expr0n [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.expr1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.expr1n [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.expr2 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.expr_div_n [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.expr_dvd [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.expr_mod [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.expr_sum [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprAC [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprB [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.exprBn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprBn_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprD [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprD1n [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprDn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprDn_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprDn_pchar [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprMn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprMn_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprMn_n [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprNn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprNn_pchar [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprS [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprSr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.exprVn [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.exprZn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.fmorph_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fmorph_eq [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fmorph_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fmorph_eq1 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fmorph_inj [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fmorph_pchar [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fmorph_unit [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fmorphV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.foldExistsP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.foldForallP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.fpred_divl [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fpred_divr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fpredMl [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.fpredMr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.holds_fsubst [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.idfun_is_monoid_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.idfun_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.IdomainMixin [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.If_form_qf [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.If_form_rf [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.imaginary_exists [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.in_alg_is_monoid_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.in_alg_is_nmod_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.in_algE [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.invf_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invfM [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr1 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr_eq1 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr_inj [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr_out [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr_sign [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invr_signM [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invrK [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invrM [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invrN [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invrN1 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.invrZ [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.iter_mulr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.iter_mulr_1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.lalgMixin [prf, in mathcomp.algebra.algebraic_hierarchy.ssralg]
GRing.lastr_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linear0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linear_closedB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linear_sum [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearD [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearMn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearMNn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearPZ [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearZ [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearZ_LR [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.linearZZ [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.lreg1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.lreg_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.lreg_sign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.lregM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.lregMl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.lregN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.lregP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.lregX [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulf_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulf_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulf_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulfI [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulfK [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulfVK [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulIf [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulIr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulIr0_rreg [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulIr_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulKf [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulKr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mull_fun_is_nmod_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mull_fun_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulN1r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulNr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr1_eq [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulr_algl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_algr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_fun_is_nmod_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_fun_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_natl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_natr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_sign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_signM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_suml [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulr_sumr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrAC [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrACA [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrBl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrBr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrCA [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrI [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulrI0_lreg [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrI_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrK [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulrN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrN1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrn_pchar [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrnAl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrnAr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrNN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.mulrVK [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulVf [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulVKf [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulVKr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.mulVr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.nat1r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.natf0_pchar [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.natf_neq0_pchar [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.natr1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.natr_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.natr_mod_pchar [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.natr_prod [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.natrB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.natrD [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.natrM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.natrX [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.nmod_morphism_semilinear [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.null_fun_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.oner_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.opp_fun_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.opp_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.oppr_pchar2 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pchar0_natf_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.pchar_lalg [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.pcharf'_nat [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.pcharf0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pcharf0P [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.pcharf_eq [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pcharf_prime [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_aut0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_aut1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_aut_is_monoid_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_aut_is_nmod_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_aut_nat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_autB_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_autD_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_autE [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_autM_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_autMn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_autN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.pFrobenius_autX [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Pick_form_qf [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.prodf_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.prodf_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.prodf_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.prodf_seq_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.prodf_seq_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.prodfV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.prodr_const [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodr_const_nat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodr_undup_exp_count [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrM_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrMl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrMl_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrMn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrMn_const [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrMr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrMr_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.prodrXl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.prodrXr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.proj_satP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.qf_evalP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.qf_to_dnf_rterm [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.qf_to_dnfP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.quantifier_elim_rformP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.quantifier_elim_wf [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.raddf_inj [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.raddfB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.raddfMnat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.raddfMNn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.raddfMsign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.raddfN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.raddfZnat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.raddfZsign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rev_prodr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rev_prodrV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rev_unitrP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.revrX [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_alg [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rmorph_eq1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_eq_nat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_nat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_pchar [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_prod [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_sign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_sum [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorph_unit [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rmorphB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphD [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphism_monoidP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphMn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphMNn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphMsign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphN1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rmorphV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rmorphXn [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpred1M [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpred_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rpred_divl [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rpred_divr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rpred_nat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpred_prod [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpred_sign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpredMl [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rpredMr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rpredMsign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpredN1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpredV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rpredX [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpredXN [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rpredZeq [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rpredZnat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rpredZsign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rreg1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rreg_neq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rregM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rregMr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rregN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.rregP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.rregX [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.same_env_sym [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.scalable_linear [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalable_semilinear [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalarP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalarZ [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.comp_op0v [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.comp_op1v [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.comp_opA [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.Scale.compN1op [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scale_fun_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scale_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaleN1r [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaleNr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.scaler_injl [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.scaler_nat [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler_prod [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler_prodl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler_prodr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler_sign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler_suml [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler_sumr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scaler_unit [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.scalerBl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerBr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerCA [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerI [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.scalerK [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.scalerKV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.scalerMnl [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerMnr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.scalerN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.sdivr_closed_div [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.sdivr_closedM [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.semilinear_linear [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.semilinearP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.semilinearPZ [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.semiring_closedD [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.semiring_closedM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.semiringClosedP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.semiscalarP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.signr_addb [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.signr_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.signr_odd [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.signrE [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.signrMK [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.signrN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.signrZK [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.size_sol [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.smulr_closedM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.smulr_closedN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.solP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.sqrf_eq0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.sqrf_eq1 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.sqrr_sign [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.sqrrB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.sqrrB1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.sqrrD [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.sqrrD1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.sqrrN [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.sub_fun_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subalg_closed_semi [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subalg_closedBM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subalg_closedZ [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subalgClosedP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.submod_closed_semi [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.submod_closedB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.submodClosedP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subr_pchar2 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subr_sqr [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subr_sqr_1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subr_sqrDB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subring_closed_semi [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subring_closedB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subring_closedM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subringClosedP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subrX1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subrXX [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subrXX_comm [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemialg_closed_subalg [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemialg_closedBM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemialg_closedM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemialg_closedZ [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemialgClosedP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemimod_closed_submod [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemimod_closedB [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemimod_closedD [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemimod_closedZ [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.subsemimodClosedP [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.telescope_prodf [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.telescope_prodf_eq [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.telescope_prodr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.telescope_prodr_eq [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.to_rform_rformula [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.to_rformP [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.to_rterm_id [prf, in mathcomp.algebra.algebraic_hierarchy.decfield]
GRing.unitfE [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitr0 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitr1 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitr_prod [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitr_prod_in [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitr_prodP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitr_sdivr_closed [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrE [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrM [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrM_comm [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrMl [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrMr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrN [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrN1 [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrPr [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrV [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrX [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.unitrX_pos [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
GRing.val1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.valM [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.valM1 [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
GRing.zmod_morphism_linear [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
gring_class_sum_central [prf, in mathcomp.group_representation.integral_char]
gring_classM_coef_sum_eq [prf, in mathcomp.group_representation.integral_char]
gring_classM_expansion [prf, in mathcomp.group_representation.integral_char]
gring_free [prf, in mathcomp.group_representation.mxrepresentation]
gring_indexK [prf, in mathcomp.group_representation.mxrepresentation]
gring_irr_modeM [prf, in mathcomp.group_representation.integral_char]
gring_mode_class_sum_eq [prf, in mathcomp.group_representation.integral_char]
gring_mxA [prf, in mathcomp.group_representation.mxrepresentation]
gring_mxJ [prf, in mathcomp.group_representation.mxrepresentation]
gring_mxK [prf, in mathcomp.group_representation.mxrepresentation]
gring_mxP [prf, in mathcomp.group_representation.mxrepresentation]
gring_op1 [prf, in mathcomp.group_representation.mxrepresentation]
gring_op_id [prf, in mathcomp.group_representation.mxrepresentation]
gring_op_mx [prf, in mathcomp.group_representation.mxrepresentation]
gring_opE [prf, in mathcomp.group_representation.mxrepresentation]
gring_opG [prf, in mathcomp.group_representation.mxrepresentation]
gring_opJ [prf, in mathcomp.group_representation.mxrepresentation]
gring_opM [prf, in mathcomp.group_representation.mxrepresentation]
gring_projE [prf, in mathcomp.group_representation.mxrepresentation]
gring_row_mul [prf, in mathcomp.group_representation.mxrepresentation]
gring_rowK [prf, in mathcomp.group_representation.mxrepresentation]
gring_valK [prf, in mathcomp.group_representation.mxrepresentation]
group0 [prf, in mathcomp.finite_group.gproduct]
group1 [prf, in mathcomp.finite_group.fingroup]
group1_contra [prf, in mathcomp.finite_group.fingroup]
group_closedM [prf, in mathcomp.boot.monoid]
group_closedV [prf, in mathcomp.boot.monoid]
group_closure_closed_field [prf, in mathcomp.group_representation.mxrepresentation]
group_closure_field_exists [prf, in mathcomp.group_representation.mxrepresentation]
group_dfwithE [prf, in mathcomp.finite_group.gproduct]
group_inj [prf, in mathcomp.finite_group.fingroup]
group_Ldiv [prf, in mathcomp.solvable.abelian]
group_modl [prf, in mathcomp.finite_group.fingroup]
group_modr [prf, in mathcomp.finite_group.fingroup]
group_not0 [prf, in mathcomp.finite_group.gproduct]
group_num_field_exists [prf, in mathcomp.group_representation.integral_char]
group_prod [prf, in mathcomp.finite_group.fingroup]
group_set_astab [prf, in mathcomp.finite_group.action]
group_set_astabs [prf, in mathcomp.finite_group.action]
group_set_bigcap [prf, in mathcomp.finite_group.fingroup]
group_set_conjG [prf, in mathcomp.finite_group.fingroup]
group_set_dfwith [prf, in mathcomp.finite_group.gproduct]
group_set_diso3 [prf, in mathcomp.solvable.burnside_app]
group_set_gacent [prf, in mathcomp.finite_group.action]
group_set_generated [prf, in mathcomp.finite_group.fingroup]
group_set_inertia [prf, in mathcomp.group_representation.inertia]
group_set_iso [prf, in mathcomp.solvable.burnside_app]
group_set_iso2 [prf, in mathcomp.solvable.burnside_app]
group_set_iso3 [prf, in mathcomp.solvable.burnside_app]
group_set_normaliser [prf, in mathcomp.finite_group.fingroup]
group_set_one [prf, in mathcomp.finite_group.fingroup]
group_set_rot [prf, in mathcomp.solvable.burnside_app]
group_set_rotations [prf, in mathcomp.solvable.burnside_app]
group_setI [prf, in mathcomp.finite_group.fingroup]
group_setJ [prf, in mathcomp.finite_group.fingroup]
group_setP [prf, in mathcomp.finite_group.fingroup]
group_setT [prf, in mathcomp.finite_group.fingroup]
group_setX [prf, in mathcomp.finite_group.gproduct]
group_setXn [prf, in mathcomp.finite_group.gproduct]
group_splitting_field_exists [prf, in mathcomp.group_representation.mxrepresentation]
groupC [prf, in mathcomp.group_representation.character]
groupD1_inj [prf, in mathcomp.finite_group.fingroup]
groupJ [prf, in mathcomp.finite_group.fingroup]
groupJr [prf, in mathcomp.finite_group.fingroup]
groupM [prf, in mathcomp.finite_group.fingroup]
groupMl [prf, in mathcomp.finite_group.fingroup]
groupMr [prf, in mathcomp.finite_group.fingroup]
groupP [prf, in mathcomp.finite_group.fingroup]
groupR [prf, in mathcomp.finite_group.fingroup]
groupV [prf, in mathcomp.finite_group.fingroup]
groupVl [prf, in mathcomp.finite_group.fingroup]
groupVr [prf, in mathcomp.finite_group.fingroup]
groupX [prf, in mathcomp.finite_group.fingroup]
groupX0 [prf, in mathcomp.finite_group.gproduct]
Grp'_dihedral [prf, in mathcomp.solvable.extremal]
Grp_2dihedral [prf, in mathcomp.solvable.extremal]
Grp_dihedral [prf, in mathcomp.solvable.extremal]
Grp_ext_dihedral [prf, in mathcomp.solvable.extremal]
Grp_modular_group [prf, in mathcomp.solvable.extremal]
Grp_pX1p2 [prf, in mathcomp.solvable.extraspecial]
Grp_quaternion [prf, in mathcomp.solvable.extremal]
Grp_semidihedral [prf, in mathcomp.solvable.extremal]
gt0 [prf, in mathcomp.algebra.interval_inference]
gt0_prodn [prf, in mathcomp.boot.bigop]
gt0_prodn_seq [prf, in mathcomp.boot.bigop]
gt0CG [prf, in mathcomp.group_representation.classfun]
gt0CiG [prf, in mathcomp.group_representation.classfun]
gt0F [prf, in mathcomp.algebra.interval_inference]
gt1F [prf, in mathcomp.algebra.interval_inference]
gt_pinfty [prf, in mathcomp.algebra.interval]
gt_rat0 [prf, in mathcomp.algebra.rat]
gt_size_poly_neq0 [prf, in mathcomp.algebra.poly]
gtn0 [prf, in mathcomp.algebra.interval_inference]
gtn_eqF [prf, in mathcomp.boot.ssrnat]
gtn_half_double [prf, in mathcomp.boot.ssrnat]
gtn_max [prf, in mathcomp.boot.ssrnat]
gtn_min [prf, in mathcomp.boot.ssrnat]
gtn_sorted_uniq_geq [prf, in mathcomp.boot.path]
gtn_uphalf_double [prf, in mathcomp.boot.ssrnat]
gtnNdvd [prf, in mathcomp.boot.div]
gtr0_sgz [prf, in mathcomp.algebra.ssrint]
gtz0_abs [prf, in mathcomp.algebra.ssrint]
gtz0_ge1 [prf, in mathcomp.algebra.ssrint]
gX_all [prf, in mathcomp.field.qfpoly]
gX_order [prf, in mathcomp.field.qfpoly]