| 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 | (76754 entries) |
| Notation 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 | (1892 entries) |
| Binder 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 | (49588 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 | (305 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 | (4034 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 | (94 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 | (14802 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 | (222 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 | (9 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 | (131 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 | (43 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 | (1392 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 | (1140 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 | (3066 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 | (36 entries) |
G
G [abbreviation, in mathcomp.character.inertia]G [abbreviation, in mathcomp.character.classfun]
G [abbreviation, in mathcomp.character.classfun]
G [abbreviation, in mathcomp.character.classfun]
g [abbreviation, in mathcomp.character.character]
gacent [definition, in mathcomp.fingroup.action]
gacentC [lemma, in mathcomp.fingroup.action]
gacentD1 [lemma, in mathcomp.fingroup.action]
gacentE [lemma, in mathcomp.fingroup.action]
gacentEsd [lemma, in mathcomp.fingroup.gproduct]
gacentIdom [lemma, in mathcomp.fingroup.action]
gacentIim [lemma, in mathcomp.fingroup.action]
gacentJ [lemma, in mathcomp.fingroup.action]
gacentM [lemma, in mathcomp.fingroup.action]
gacentQ [lemma, in mathcomp.fingroup.action]
gacentS [lemma, in mathcomp.fingroup.action]
gacentU [lemma, in mathcomp.fingroup.action]
gacentY [lemma, in mathcomp.fingroup.action]
gacent_comp [lemma, in mathcomp.fingroup.action]
gacent_mod [lemma, in mathcomp.fingroup.action]
gacent_actby [lemma, in mathcomp.fingroup.action]
gacent_ract [lemma, in mathcomp.fingroup.action]
gacent_cycle [lemma, in mathcomp.fingroup.action]
gacent_gen [lemma, in mathcomp.fingroup.action]
gacent_group [definition, in mathcomp.fingroup.action]
gacent_repr [lemma, in mathcomp.character.mxabelem]
gacent1 [lemma, in mathcomp.fingroup.action]
gacent1E [lemma, in mathcomp.fingroup.action]
gact [projection, in mathcomp.fingroup.action]
gactJ [lemma, in mathcomp.fingroup.action]
gactM [lemma, in mathcomp.fingroup.action]
gactR [lemma, in mathcomp.fingroup.action]
gactsI [lemma, in mathcomp.solvable.jordanholder]
gactsM [lemma, in mathcomp.solvable.jordanholder]
gactsP [lemma, in mathcomp.solvable.jordanholder]
gacts_char [lemma, in mathcomp.fingroup.action]
gacts_range [lemma, in mathcomp.fingroup.action]
gactV [lemma, in mathcomp.fingroup.action]
gactX [lemma, in mathcomp.fingroup.action]
gact_stable [lemma, in mathcomp.fingroup.action]
gact_out [lemma, in mathcomp.fingroup.action]
gact_range [definition, in mathcomp.fingroup.action]
gact1 [lemma, in mathcomp.fingroup.action]
gal [definition, in mathcomp.field.galois]
Gal [constructor, in mathcomp.field.galois]
galK [lemma, in mathcomp.field.galois]
galLgen [lemma, in mathcomp.field.finfield]
galL:112 [binder, in mathcomp.field.finfield]
galM [lemma, in mathcomp.field.galois]
galNorm [definition, in mathcomp.field.galois]
galNormM [lemma, in mathcomp.field.galois]
galNormV [lemma, in mathcomp.field.galois]
galNormX [lemma, in mathcomp.field.galois]
galNorm_gal [lemma, in mathcomp.field.galois]
galNorm_fixedField [lemma, in mathcomp.field.galois]
galNorm_eq0 [lemma, in mathcomp.field.galois]
galNorm_prod [lemma, in mathcomp.field.galois]
galNorm0 [lemma, in mathcomp.field.galois]
galNorm1 [lemma, in mathcomp.field.galois]
galois [definition, in mathcomp.field.galois]
galois [library]
galoisG [definition, in mathcomp.field.galois]
galoisG_group [definition, in mathcomp.field.galois]
galoisS [lemma, in mathcomp.field.galois]
GaloisTheory [section, in mathcomp.field.galois]
GaloisTheory.Automorphism [section, in mathcomp.field.galois]
GaloisTheory.F [variable, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory [section, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.E [variable, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.galKE [variable, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.IntermediateField [section, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.IntermediateField.M [variable, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.IntermediateField.nKM [variable, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.IntermediateField.sKME [variable, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.IntermediateGroup [section, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.IntermediateGroup.G [variable, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.IntermediateGroup.nsGgalE [variable, in mathcomp.field.galois]
GaloisTheory.FundamentalTheoremOfGaloisTheory.K [variable, in mathcomp.field.galois]
GaloisTheory.gal_of_Definition.gal_sgval_inj [variable, in mathcomp.field.galois]
GaloisTheory.gal_of_Definition.V [variable, in mathcomp.field.galois]
GaloisTheory.gal_of_Definition [section, in mathcomp.field.galois]
GaloisTheory.L [variable, in mathcomp.field.galois]
GaloisTheory.Matrix [section, in mathcomp.field.galois]
GaloisTheory.Matrix.A [variable, in mathcomp.field.galois]
GaloisTheory.Matrix.E [variable, in mathcomp.field.galois]
GaloisTheory.Matrix.K [variable, in mathcomp.field.galois]
GaloisTheory.TraceAndNormField [section, in mathcomp.field.galois]
GaloisTheory.TraceAndNormField.E [variable, in mathcomp.field.galois]
GaloisTheory.TraceAndNormField.K [variable, in mathcomp.field.galois]
GaloisTheory.TraceAndNormMorphism [section, in mathcomp.field.galois]
GaloisTheory.TraceAndNormMorphism.U [variable, in mathcomp.field.galois]
GaloisTheory.TraceAndNormMorphism.V [variable, in mathcomp.field.galois]
'Gal ( _ / _ ) (Group_scope) [notation, in mathcomp.field.galois]
'Gal ( _ / _ ) (group_scope) [notation, in mathcomp.field.galois]
galois_fixedField [lemma, in mathcomp.field.galois]
galois_factors [lemma, in mathcomp.field.galois]
galois_dim [lemma, in mathcomp.field.galois]
galois_connection [lemma, in mathcomp.field.galois]
galois_connection_subset [lemma, in mathcomp.field.galois]
galois_connection_subv [lemma, in mathcomp.field.galois]
galS [lemma, in mathcomp.field.galois]
galTrace [definition, in mathcomp.field.galois]
galTrace_gal [lemma, in mathcomp.field.galois]
galTrace_fixedField [lemma, in mathcomp.field.galois]
galTrace_is_additive [lemma, in mathcomp.field.galois]
galV [lemma, in mathcomp.field.galois]
gal_generated [lemma, in mathcomp.field.galois]
gal_fixedField [lemma, in mathcomp.field.galois]
gal_matrix [lemma, in mathcomp.field.galois]
gal_independent [lemma, in mathcomp.field.galois]
gal_independent_contra [lemma, in mathcomp.field.galois]
gal_conjg [lemma, in mathcomp.field.galois]
gal_adjoin_eq [lemma, in mathcomp.field.galois]
gal_kHom [lemma, in mathcomp.field.galois]
gal_kAut [lemma, in mathcomp.field.galois]
gal_cap [lemma, in mathcomp.field.galois]
gal_id [lemma, in mathcomp.field.galois]
gal_eqP [lemma, in mathcomp.field.galois]
gal_AEnd [lemma, in mathcomp.field.galois]
gal_repr_inj [lemma, in mathcomp.field.galois]
gal_reprK [lemma, in mathcomp.field.galois]
gal_morphism [definition, in mathcomp.field.galois]
gal_is_morphism [lemma, in mathcomp.field.galois]
gal_repr [definition, in mathcomp.field.galois]
gal_mulP [lemma, in mathcomp.field.galois]
gal_invP [lemma, in mathcomp.field.galois]
gal_oneP [lemma, in mathcomp.field.galois]
gal_mul [definition, in mathcomp.field.galois]
gal_inv [definition, in mathcomp.field.galois]
gal_one [definition, in mathcomp.field.galois]
gal_sgvalK [lemma, in mathcomp.field.galois]
gal_sgval [definition, in mathcomp.field.galois]
gal_of [inductive, in mathcomp.field.galois]
Gaschutz [section, in mathcomp.solvable.finmodule]
Gaschutz_transitive [lemma, in mathcomp.solvable.finmodule]
Gaschutz_split [lemma, in mathcomp.solvable.finmodule]
Gaschutz.abelH [variable, in mathcomp.solvable.finmodule]
Gaschutz.coHiPG [variable, in mathcomp.solvable.finmodule]
Gaschutz.G [variable, in mathcomp.solvable.finmodule]
Gaschutz.gT [variable, in mathcomp.solvable.finmodule]
Gaschutz.H [variable, in mathcomp.solvable.finmodule]
Gaschutz.m [variable, in mathcomp.solvable.finmodule]
Gaschutz.nHG [variable, in mathcomp.solvable.finmodule]
Gaschutz.nsHG [variable, in mathcomp.solvable.finmodule]
Gaschutz.P [variable, in mathcomp.solvable.finmodule]
Gaschutz.sHG [variable, in mathcomp.solvable.finmodule]
Gaschutz.sHP [variable, in mathcomp.solvable.finmodule]
Gaschutz.sPG [variable, in mathcomp.solvable.finmodule]
gastabsP [lemma, in mathcomp.solvable.jordanholder]
GaussE [abbreviation, in mathcomp.algebra.mxalgebra]
Gaussian_elimination_map [lemma, in mathcomp.algebra.mxalgebra]
Gaussian_elimination_unlockable [definition, in mathcomp.algebra.mxalgebra]
Gaussian_elimination_ [definition, in mathcomp.algebra.mxalgebra]
Gauss_gcdl [lemma, in mathcomp.ssreflect.div]
Gauss_gcdr [lemma, in mathcomp.ssreflect.div]
Gauss_dvdl [lemma, in mathcomp.ssreflect.div]
Gauss_dvdr [lemma, in mathcomp.ssreflect.div]
Gauss_dvd [lemma, in mathcomp.ssreflect.div]
Gauss_gcdzl [lemma, in mathcomp.algebra.intdiv]
Gauss_gcdzr [lemma, in mathcomp.algebra.intdiv]
Gauss_dvdzl [lemma, in mathcomp.algebra.intdiv]
Gauss_dvdzr [lemma, in mathcomp.algebra.intdiv]
Gauss_dvdz [lemma, in mathcomp.algebra.intdiv]
gA:554 [binder, in mathcomp.fingroup.fingroup]
gcard [definition, in mathcomp.character.mxrepresentation]
gcdn [definition, in mathcomp.ssreflect.div]
gcdnA [lemma, in mathcomp.ssreflect.div]
gcdnAC [lemma, in mathcomp.ssreflect.div]
gcdnACA [lemma, in mathcomp.ssreflect.div]
gcdnC [lemma, in mathcomp.ssreflect.div]
gcdnCA [lemma, in mathcomp.ssreflect.div]
gcdnDl [lemma, in mathcomp.ssreflect.div]
gcdnDr [lemma, in mathcomp.ssreflect.div]
gcdnE [lemma, in mathcomp.ssreflect.div]
gcdnMDl [lemma, in mathcomp.ssreflect.div]
gcdnMl [lemma, in mathcomp.ssreflect.div]
gcdnMr [lemma, in mathcomp.ssreflect.div]
gcdnn [lemma, in mathcomp.ssreflect.div]
gcdNz [lemma, in mathcomp.algebra.intdiv]
gcdn_def [lemma, in mathcomp.ssreflect.div]
gcdn_modl [lemma, in mathcomp.ssreflect.div]
gcdn_modr [lemma, in mathcomp.ssreflect.div]
gcdn_idPr [lemma, in mathcomp.ssreflect.div]
gcdn_idPl [lemma, in mathcomp.ssreflect.div]
gcdn_gt0 [lemma, in mathcomp.ssreflect.div]
gcdn_rec [definition, in mathcomp.ssreflect.div]
gcdn0 [lemma, in mathcomp.ssreflect.div]
gcdn1 [lemma, in mathcomp.ssreflect.div]
gcdp_polyOver [lemma, in mathcomp.field.fieldext]
gcdz [definition, in mathcomp.algebra.intdiv]
gcdzA [lemma, in mathcomp.algebra.intdiv]
gcdzAC [lemma, in mathcomp.algebra.intdiv]
gcdzACA [lemma, in mathcomp.algebra.intdiv]
gcdzC [lemma, in mathcomp.algebra.intdiv]
gcdzCA [lemma, in mathcomp.algebra.intdiv]
gcdzDl [lemma, in mathcomp.algebra.intdiv]
gcdzDr [lemma, in mathcomp.algebra.intdiv]
gcdzMDl [lemma, in mathcomp.algebra.intdiv]
gcdzMl [lemma, in mathcomp.algebra.intdiv]
gcdzMr [lemma, in mathcomp.algebra.intdiv]
gcdzN [lemma, in mathcomp.algebra.intdiv]
gcdzz [lemma, in mathcomp.algebra.intdiv]
gcdz_idPr [lemma, in mathcomp.algebra.intdiv]
gcdz_idPl [lemma, in mathcomp.algebra.intdiv]
gcdz_modl [lemma, in mathcomp.algebra.intdiv]
gcdz_modr [lemma, in mathcomp.algebra.intdiv]
gcdz_eq0 [lemma, in mathcomp.algebra.intdiv]
gcdz0 [lemma, in mathcomp.algebra.intdiv]
gcdz1 [lemma, in mathcomp.algebra.intdiv]
gcd0n [lemma, in mathcomp.ssreflect.div]
gcd0z [lemma, in mathcomp.algebra.intdiv]
gcd1n [lemma, in mathcomp.ssreflect.div]
gcd1z [lemma, in mathcomp.algebra.intdiv]
gcore [definition, in mathcomp.fingroup.fingroup]
gcore_max [lemma, in mathcomp.fingroup.fingroup]
gcore_normal [lemma, in mathcomp.fingroup.fingroup]
gcore_norm [lemma, in mathcomp.fingroup.fingroup]
gcore_sub [lemma, in mathcomp.fingroup.fingroup]
gcore_group [definition, in mathcomp.fingroup.fingroup]
geigenspace [definition, in mathcomp.algebra.mxpoly]
geigenspaceE [lemma, in mathcomp.algebra.mxpoly]
genD [lemma, in mathcomp.fingroup.fingroup]
genDU [lemma, in mathcomp.fingroup.fingroup]
genD1 [lemma, in mathcomp.fingroup.fingroup]
genD1id [lemma, in mathcomp.fingroup.fingroup]
GeneralExponentPextraspecialTheory [section, in mathcomp.solvable.extraspecial]
GeneralExponentPextraspecialTheory.p [variable, in mathcomp.solvable.extraspecial]
generalized_orthogonality_relation [lemma, in mathcomp.character.character]
GeneratedGroup [section, in mathcomp.fingroup.fingroup]
GeneratedGroup.gT [variable, in mathcomp.fingroup.fingroup]
generatedP [lemma, in mathcomp.fingroup.fingroup]
generated_group [definition, in mathcomp.fingroup.fingroup]
generated_unlockable [definition, in mathcomp.fingroup.fingroup]
generator [definition, in mathcomp.solvable.cyclic]
generators_quaternion [lemma, in mathcomp.solvable.extremal]
generators_semidihedral [lemma, in mathcomp.solvable.extremal]
generators_2dihedral [lemma, in mathcomp.solvable.extremal]
generators_modular_group [lemma, in mathcomp.solvable.extremal]
generator_coprime [lemma, in mathcomp.solvable.cyclic]
generator_order [lemma, in mathcomp.solvable.cyclic]
generator_cycle [lemma, in mathcomp.solvable.cyclic]
GenericClassSums [section, in mathcomp.character.integral_char]
GenericClassSums.F [variable, in mathcomp.character.integral_char]
GenericClassSums.G [variable, in mathcomp.character.integral_char]
GenericClassSums.gT [variable, in mathcomp.character.integral_char]
'K_ _ (ring_scope) [notation, in mathcomp.character.integral_char]
generic_quotient [library]
genGid [lemma, in mathcomp.fingroup.fingroup]
genGidG [lemma, in mathcomp.fingroup.fingroup]
genJ [lemma, in mathcomp.fingroup.fingroup]
genmxE [lemma, in mathcomp.algebra.mxalgebra]
genmxP [lemma, in mathcomp.algebra.mxalgebra]
genmx_Socle [lemma, in mathcomp.character.mxrepresentation]
genmx_component [lemma, in mathcomp.character.mxrepresentation]
genmx_muls [lemma, in mathcomp.algebra.mxalgebra]
genmx_diff [lemma, in mathcomp.algebra.mxalgebra]
genmx_bigcap [lemma, in mathcomp.algebra.mxalgebra]
genmx_cap [lemma, in mathcomp.algebra.mxalgebra]
genmx_sums [lemma, in mathcomp.algebra.mxalgebra]
genmx_adds [lemma, in mathcomp.algebra.mxalgebra]
genmx_id [lemma, in mathcomp.algebra.mxalgebra]
genmx_unlockable [definition, in mathcomp.algebra.mxalgebra]
genmx_witness [definition, in mathcomp.algebra.mxalgebra]
genmx0 [lemma, in mathcomp.algebra.mxalgebra]
genmx1 [lemma, in mathcomp.algebra.mxalgebra]
genM_join [lemma, in mathcomp.fingroup.fingroup]
genS [lemma, in mathcomp.fingroup.fingroup]
GenTree [module, in mathcomp.ssreflect.choice]
GenTree.codeK [lemma, in mathcomp.ssreflect.choice]
GenTree.decode [definition, in mathcomp.ssreflect.choice]
GenTree.decode_step [definition, in mathcomp.ssreflect.choice]
GenTree.Def [section, in mathcomp.ssreflect.choice]
GenTree.Def.T [variable, in mathcomp.ssreflect.choice]
GenTree.encode [definition, in mathcomp.ssreflect.choice]
GenTree.Leaf [constructor, in mathcomp.ssreflect.choice]
GenTree.Node [constructor, in mathcomp.ssreflect.choice]
GenTree.tree [inductive, in mathcomp.ssreflect.choice]
GenTree.tree_ind [definition, in mathcomp.ssreflect.choice]
GenTree.tree_rec [definition, in mathcomp.ssreflect.choice]
GenTree.tree_rect [definition, in mathcomp.ssreflect.choice]
genV [lemma, in mathcomp.fingroup.fingroup]
gen_prodgP [lemma, in mathcomp.fingroup.fingroup]
gen_expgs [lemma, in mathcomp.fingroup.fingroup]
gen_set_id [lemma, in mathcomp.fingroup.fingroup]
gen_subG [lemma, in mathcomp.fingroup.fingroup]
gen_rank [definition, in mathcomp.solvable.abelian]
gen_diso3 [lemma, in mathcomp.solvable.burnside_app]
gen0 [lemma, in mathcomp.fingroup.fingroup]
geq [definition, in mathcomp.ssreflect.ssrnat]
GeqNotLtn [constructor, in mathcomp.ssreflect.ssrnat]
geq_divBl [lemma, in mathcomp.ssreflect.div]
geq_leqif [lemma, in mathcomp.ssreflect.ssrnat]
geq_uphalf_double [lemma, in mathcomp.ssreflect.ssrnat]
geq_half_double [lemma, in mathcomp.ssreflect.ssrnat]
geq_minr [lemma, in mathcomp.ssreflect.ssrnat]
geq_minl [lemma, in mathcomp.ssreflect.ssrnat]
geq_min [lemma, in mathcomp.ssreflect.ssrnat]
geq_max [lemma, in mathcomp.ssreflect.ssrnat]
ger_total:2501 [binder, in mathcomp.algebra.ssrnum]
ger_leVge:27 [binder, in mathcomp.algebra.ssrnum]
getCratK [lemma, in mathcomp.field.algC]
gez0_abs [lemma, in mathcomp.algebra.ssrint]
ge_pinfty [lemma, in mathcomp.algebra.interval]
ge_rat0_norm [lemma, in mathcomp.algebra.rat]
ge_rat0 [lemma, in mathcomp.algebra.rat]
ge0_norm:2595 [binder, in mathcomp.algebra.ssrnum]
ge0_norm:2555 [binder, in mathcomp.algebra.ssrnum]
gFchar [lemma, in mathcomp.solvable.gfunctor]
gFchar_trans [lemma, in mathcomp.solvable.gfunctor]
gFcompS [lemma, in mathcomp.solvable.gfunctor]
gFcomp_mgFun [definition, in mathcomp.solvable.gfunctor]
gFcomp_gFun [definition, in mathcomp.solvable.gfunctor]
gFcomp_igFun [definition, in mathcomp.solvable.gfunctor]
gFcomp_cont [lemma, in mathcomp.solvable.gfunctor]
gFcomp_closed [lemma, in mathcomp.solvable.gfunctor]
gFcont [lemma, in mathcomp.solvable.gfunctor]
gFgroup [definition, in mathcomp.solvable.gfunctor]
gFgroupset [lemma, in mathcomp.solvable.gfunctor]
gFhereditary [lemma, in mathcomp.solvable.gfunctor]
gFid [lemma, in mathcomp.solvable.gfunctor]
gFisog [lemma, in mathcomp.solvable.gfunctor]
gFisom [lemma, in mathcomp.solvable.gfunctor]
gFiso_cont [lemma, in mathcomp.solvable.gfunctor]
gFmod_pgFun [definition, in mathcomp.solvable.gfunctor]
gFmod_hereditary [lemma, in mathcomp.solvable.gfunctor]
gFmod_gFun [definition, in mathcomp.solvable.gfunctor]
gFmod_igFun [definition, in mathcomp.solvable.gfunctor]
gFmod_cont [lemma, in mathcomp.solvable.gfunctor]
gFmod_closed [lemma, in mathcomp.solvable.gfunctor]
gFmod_group [definition, in mathcomp.solvable.gfunctor]
gFnorm [lemma, in mathcomp.solvable.gfunctor]
gFnormal [lemma, in mathcomp.solvable.gfunctor]
gFnormal_trans [lemma, in mathcomp.solvable.gfunctor]
gFnorms [lemma, in mathcomp.solvable.gfunctor]
gFnorm_trans [lemma, in mathcomp.solvable.gfunctor]
gFsub [lemma, in mathcomp.solvable.gfunctor]
gFsub_trans [lemma, in mathcomp.solvable.gfunctor]
GFunctor [module, in mathcomp.solvable.gfunctor]
gfunctor [library]
GFunctorExamples [section, in mathcomp.solvable.gfunctor]
gFunctorI [lemma, in mathcomp.solvable.gfunctor]
gFunctorS [lemma, in mathcomp.solvable.gfunctor]
GFunctor.apply [projection, in mathcomp.solvable.gfunctor]
GFunctor.ClassDefinitions [section, in mathcomp.solvable.gfunctor]
GFunctor.clone [definition, in mathcomp.solvable.gfunctor]
GFunctor.clone_mono [definition, in mathcomp.solvable.gfunctor]
GFunctor.clone_pmap [definition, in mathcomp.solvable.gfunctor]
GFunctor.clone_iso [definition, in mathcomp.solvable.gfunctor]
GFunctor.closed [definition, in mathcomp.solvable.gfunctor]
GFunctor.comp [definition, in mathcomp.solvable.gfunctor]
GFunctor.continuous [definition, in mathcomp.solvable.gfunctor]
GFunctor.continuous_is_iso_continuous [lemma, in mathcomp.solvable.gfunctor]
GFunctor.Definitions [section, in mathcomp.solvable.gfunctor]
GFunctor.Definitions.F [variable, in mathcomp.solvable.gfunctor]
GFunctor.Definitions.F1 [variable, in mathcomp.solvable.gfunctor]
GFunctor.Definitions.F2 [variable, in mathcomp.solvable.gfunctor]
GFunctor.Definitions.k [variable, in mathcomp.solvable.gfunctor]
GFunctor.Exports [module, in mathcomp.solvable.gfunctor]
[ mgFun of _ ] (form_scope) [notation, in mathcomp.solvable.gfunctor]
[ mgFun by _ ] (form_scope) [notation, in mathcomp.solvable.gfunctor]
[ pgFun of _ ] (form_scope) [notation, in mathcomp.solvable.gfunctor]
[ pgFun by _ ] (form_scope) [notation, in mathcomp.solvable.gfunctor]
[ gFun of _ ] (form_scope) [notation, in mathcomp.solvable.gfunctor]
[ gFun by _ ] (form_scope) [notation, in mathcomp.solvable.gfunctor]
[ igFun of _ ] (form_scope) [notation, in mathcomp.solvable.gfunctor]
[ igFun by _ & ! _ ] (form_scope) [notation, in mathcomp.solvable.gfunctor]
[ igFun by _ & _ ] (form_scope) [notation, in mathcomp.solvable.gfunctor]
GFunctor.group_valued [definition, in mathcomp.solvable.gfunctor]
GFunctor.hereditary [definition, in mathcomp.solvable.gfunctor]
GFunctor.iso_of_map [projection, in mathcomp.solvable.gfunctor]
GFunctor.iso_map [record, in mathcomp.solvable.gfunctor]
GFunctor.iso_continuous [definition, in mathcomp.solvable.gfunctor]
GFunctor.map [record, in mathcomp.solvable.gfunctor]
GFunctor.map_of_mono [projection, in mathcomp.solvable.gfunctor]
GFunctor.map_of_pmap [projection, in mathcomp.solvable.gfunctor]
GFunctor.modulo [definition, in mathcomp.solvable.gfunctor]
GFunctor.monotonic [definition, in mathcomp.solvable.gfunctor]
GFunctor.mono_map [record, in mathcomp.solvable.gfunctor]
GFunctor.object_map [definition, in mathcomp.solvable.gfunctor]
GFunctor.pack_iso [definition, in mathcomp.solvable.gfunctor]
GFunctor.pcontinuous [definition, in mathcomp.solvable.gfunctor]
GFunctor.pcontinuous_is_hereditary [lemma, in mathcomp.solvable.gfunctor]
GFunctor.pcontinuous_is_continuous [lemma, in mathcomp.solvable.gfunctor]
GFunctor.pmap [record, in mathcomp.solvable.gfunctor]
gFunc_id [definition, in mathcomp.solvable.gfunctor]
gF1 [lemma, in mathcomp.solvable.gfunctor]
gf:2275 [binder, in mathcomp.algebra.matrix]
gf:2282 [binder, in mathcomp.algebra.matrix]
gH [abbreviation, in mathcomp.fingroup.gproduct]
GH:149 [binder, in mathcomp.solvable.center]
gK [abbreviation, in mathcomp.fingroup.gproduct]
GK:150 [binder, in mathcomp.solvable.center]
GLgroup [definition, in mathcomp.algebra.matrix]
GLgroup_group [definition, in mathcomp.algebra.matrix]
GLmx_faithful [lemma, in mathcomp.character.mxabelem]
GLrepr [definition, in mathcomp.character.mxabelem]
GLtype [definition, in mathcomp.algebra.matrix]
GLval [definition, in mathcomp.algebra.matrix]
GL_det [lemma, in mathcomp.algebra.matrix]
GL_unitmx [lemma, in mathcomp.algebra.matrix]
GL_unit [lemma, in mathcomp.algebra.matrix]
GL_MxE [lemma, in mathcomp.algebra.matrix]
GL_ME [lemma, in mathcomp.algebra.matrix]
GL_VxE [lemma, in mathcomp.algebra.matrix]
GL_VE [lemma, in mathcomp.algebra.matrix]
GL_1E [lemma, in mathcomp.algebra.matrix]
GL_unit.R [variable, in mathcomp.algebra.matrix]
GL_unit.n [variable, in mathcomp.algebra.matrix]
GL_unit [section, in mathcomp.algebra.matrix]
GL_mx_repr [lemma, in mathcomp.character.mxabelem]
gnorm [definition, in mathcomp.fingroup.fingroup]
gof [abbreviation, in mathcomp.fingroup.morphism]
gproduct [library]
gP:1297 [binder, in mathcomp.fingroup.fingroup]
gP:1300 [binder, in mathcomp.fingroup.fingroup]
gp:299 [binder, in mathcomp.field.closed_field]
graded:471 [binder, in mathcomp.ssreflect.path]
grank_abelian [lemma, in mathcomp.solvable.abelian]
grank_witness [lemma, in mathcomp.solvable.abelian]
grank_min [lemma, in mathcomp.solvable.abelian]
grel [definition, in mathcomp.ssreflect.fingraph]
grepr0 [definition, in mathcomp.character.character]
GRing [module, in mathcomp.algebra.ssralg]
gring_classM_coef_sum_eq [lemma, in mathcomp.character.integral_char]
gring_mode_class_sum_eq [lemma, in mathcomp.character.integral_char]
gring_irr_modeM [lemma, in mathcomp.character.integral_char]
gring_irr_mode_unlockable [definition, in mathcomp.character.integral_char]
gring_classM_expansion [lemma, in mathcomp.character.integral_char]
gring_class_sum_central [lemma, in mathcomp.character.integral_char]
gring_class_sum [definition, in mathcomp.character.integral_char]
gring_classM_coef [definition, in mathcomp.character.integral_char]
gring_classM_coef_set [definition, in mathcomp.character.integral_char]
gring_opM [lemma, in mathcomp.character.mxrepresentation]
gring_mxP [lemma, in mathcomp.character.mxrepresentation]
gring_rowK [lemma, in mathcomp.character.mxrepresentation]
gring_op_id [lemma, in mathcomp.character.mxrepresentation]
gring_free [lemma, in mathcomp.character.mxrepresentation]
gring_mxA [lemma, in mathcomp.character.mxrepresentation]
gring_op_mx [lemma, in mathcomp.character.mxrepresentation]
gring_opJ [lemma, in mathcomp.character.mxrepresentation]
gring_op1 [lemma, in mathcomp.character.mxrepresentation]
gring_opG [lemma, in mathcomp.character.mxrepresentation]
gring_opE [lemma, in mathcomp.character.mxrepresentation]
gring_op [definition, in mathcomp.character.mxrepresentation]
gring_mxK [lemma, in mathcomp.character.mxrepresentation]
gring_mxJ [lemma, in mathcomp.character.mxrepresentation]
gring_mx [definition, in mathcomp.character.mxrepresentation]
gring_projE [lemma, in mathcomp.character.mxrepresentation]
gring_proj [definition, in mathcomp.character.mxrepresentation]
gring_row_mul [lemma, in mathcomp.character.mxrepresentation]
gring_row [definition, in mathcomp.character.mxrepresentation]
gring_indexK [lemma, in mathcomp.character.mxrepresentation]
gring_valK [lemma, in mathcomp.character.mxrepresentation]
gring_index [definition, in mathcomp.character.mxrepresentation]
GRing.Add [constructor, in mathcomp.algebra.ssralg]
GRing.addf_div [lemma, in mathcomp.algebra.ssralg]
GRing.addIr [lemma, in mathcomp.algebra.ssralg]
GRing.additive [section, in mathcomp.algebra.ssralg]
GRing.additive [section, in mathcomp.algebra.ssralg]
GRing.additive [definition, in mathcomp.algebra.ssralg]
GRing.AdditiveExports [module, in mathcomp.algebra.ssralg]
GRing.AdditiveExports.Additive [module, in mathcomp.algebra.ssralg]
GRing.AdditiveExports.Additive.apply [abbreviation, in mathcomp.algebra.ssralg]
GRing.AdditiveExports.Additive.apply_deprecated [definition, in mathcomp.algebra.ssralg]
[ additive of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ additive of _ as _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
{ additive _ -> _ } (type_scope) [notation, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory [section, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun [section, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun [section, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.f [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.f [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.g [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.g [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.h [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.h [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.U [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.U [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.V [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.V [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.W [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.AddFun.W [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.MulFun [section, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.MulFun.a [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.MulFun.f [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.MulFun.R [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.MulFun.U [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties [section, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties [section, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties.f [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties.f [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties.k [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties.k [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties.U [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties.U [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties.V [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.Properties.V [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.RingProperties [section, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.RingProperties.f [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.RingProperties.h [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.RingProperties.R [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.RingProperties.S [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.RingProperties.U [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.RingProperties.V [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.ScaleFun [section, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.ScaleFun.a [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.ScaleFun.f [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.ScaleFun.R [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.ScaleFun.U [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.ScaleFun.V [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.SemiRingProperties [section, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.SemiRingProperties.f [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.SemiRingProperties.R [variable, in mathcomp.algebra.ssralg]
GRing.AdditiveTheory.SemiRingProperties.S [variable, in mathcomp.algebra.ssralg]
GRing.additive_linear [lemma, in mathcomp.algebra.ssralg]
GRing.addKr [lemma, in mathcomp.algebra.ssralg]
GRing.addKr_char2 [lemma, in mathcomp.algebra.ssralg]
GRing.addNKr [lemma, in mathcomp.algebra.ssralg]
GRing.addrAC [lemma, in mathcomp.algebra.ssralg]
GRing.addrACA [lemma, in mathcomp.algebra.ssralg]
GRing.addrCA [lemma, in mathcomp.algebra.ssralg]
GRing.addrI [lemma, in mathcomp.algebra.ssralg]
GRing.addrK [lemma, in mathcomp.algebra.ssralg]
GRing.addrKA [lemma, in mathcomp.algebra.ssralg]
GRing.addrK_char2 [lemma, in mathcomp.algebra.ssralg]
GRing.addrN [lemma, in mathcomp.algebra.ssralg]
GRing.addrNK [lemma, in mathcomp.algebra.ssralg]
GRing.addrr_char2 [lemma, in mathcomp.algebra.ssralg]
GRing.addr_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.addr_closed [definition, in mathcomp.algebra.ssralg]
GRing.addr0 [lemma, in mathcomp.algebra.ssralg]
GRing.addr0_eq [lemma, in mathcomp.algebra.ssralg]
GRing.add_fun_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.add_fun_is_semi_additive [lemma, in mathcomp.algebra.ssralg]
GRing.add_fun [definition, in mathcomp.algebra.ssralg]
GRing.AlgebraTheory [section, in mathcomp.algebra.ssralg]
GRing.AlgebraTheory [section, in mathcomp.algebra.ssralg]
GRing.AlgebraTheory.a [variable, in mathcomp.algebra.ssralg]
GRing.AlgebraTheory.A [variable, in mathcomp.algebra.ssralg]
GRing.AlgebraTheory.f [variable, in mathcomp.algebra.ssralg]
GRing.AlgebraTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.AlgebraTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.AlgebraTheory.U [variable, in mathcomp.algebra.ssralg]
GRing.AlgExports [module, in mathcomp.algebra.ssralg]
[ algType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ algType _ of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.algMixin [lemma, in mathcomp.algebra.ssralg]
GRing.AllExports [module, in mathcomp.algebra.ssralg]
GRing.And [constructor, in mathcomp.algebra.ssralg]
GRing.and_dnfP [lemma, in mathcomp.algebra.ssralg]
GRing.and_dnf [definition, in mathcomp.algebra.ssralg]
GRing.bin_lt_charf_0 [lemma, in mathcomp.algebra.ssralg]
GRing.Bool [constructor, in mathcomp.algebra.ssralg]
GRing.Builders_560.fieldP [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_555.id [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_538.invr_out [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_538.unitrP [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_538.divrr [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_538.mulVr [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_538.Builders_538.invU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_538.Builders_538.inU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_533.scalerAr [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_528.scalerAl [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_514.valZ [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_514.scalerDl [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_514.scalerDr [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_514.scale1r [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_514.scalerA' [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_514.Builders_514.scaleW [variable, in mathcomp.algebra.ssralg]
GRing.Builders_514.Builders_514.inW [variable, in mathcomp.algebra.ssralg]
GRing.Builders_507.mulrC [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_492.Builders_492.mulU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_492.Builders_492.oneU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_492.Builders_492.inU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_487.mulrC [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.valM [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.oner_neq0 [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.mulr0 [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.mul0r [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.mulrDr [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.mulrDl [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.mulr1 [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.mul1r [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.mulrA [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_475.Builders_475.mulU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_475.Builders_475.oneU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_475.Builders_475.inU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_457.valB [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_457.valD [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_457.addNr [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_457.Builders_457.addU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_457.Builders_457.oppU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_457.Builders_457.zeroU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_457.Builders_457.inU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_445.valD [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_445.val0 [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_445.add0U [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_445.addUC [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_445.addUA [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_445.Builders_445.addU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_445.Builders_445.zeroU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_445.Builders_445.inU [variable, in mathcomp.algebra.ssralg]
GRing.Builders_322.inv_out [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_322.intro_unit [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_263.mulC_unitP [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_263.mulC_mulrV [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_233.scalarAr [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_216.mulrDr [definition, in mathcomp.algebra.ssralg]
GRing.Builders_216.mulr1 [definition, in mathcomp.algebra.ssralg]
GRing.Builders_203.mulr0 [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_203.mulrDr [definition, in mathcomp.algebra.ssralg]
GRing.Builders_203.mulr1 [definition, in mathcomp.algebra.ssralg]
GRing.Builders_110.raddfD [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_110.raddf0 [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_33.mulr0 [lemma, in mathcomp.algebra.ssralg]
GRing.Builders_33.mul0r [lemma, in mathcomp.algebra.ssralg]
_ * _ [notation, in mathcomp.algebra.ssralg]
1 [notation, in mathcomp.algebra.ssralg]
GRing.can2_linear [lemma, in mathcomp.algebra.ssralg]
GRing.can2_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.can2_rmorphism [lemma, in mathcomp.algebra.ssralg]
GRing.can2_additive [lemma, in mathcomp.algebra.ssralg]
GRing.can2_semi_additive [lemma, in mathcomp.algebra.ssralg]
GRing.cat_dnfP [lemma, in mathcomp.algebra.ssralg]
GRing.char [definition, in mathcomp.algebra.ssralg]
GRing.charf_eq [lemma, in mathcomp.algebra.ssralg]
GRing.charf_prime [lemma, in mathcomp.algebra.ssralg]
GRing.charf'_nat [lemma, in mathcomp.algebra.ssralg]
GRing.charf0 [lemma, in mathcomp.algebra.ssralg]
GRing.charf0P [lemma, in mathcomp.algebra.ssralg]
GRing.char_lalg [lemma, in mathcomp.algebra.ssralg]
GRing.char0_natf_div [lemma, in mathcomp.algebra.ssralg]
GRing.ClosedExports [module, in mathcomp.algebra.ssralg]
GRing.ClosedExports.addr_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.divalg_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.divring_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.divr_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.invr_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.linear_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.mulr_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.oppr_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.scaler_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.sdivr_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.semiring_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.smulr_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.subalg_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.submod_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.subring_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedExports.zmod_closed [abbreviation, in mathcomp.algebra.ssralg]
GRing.ClosedFieldExports [module, in mathcomp.algebra.ssralg]
[ closedFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ closedFieldType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.ClosedFieldTheory [section, in mathcomp.algebra.ssralg]
GRing.ClosedFieldTheory.F [variable, in mathcomp.algebra.ssralg]
GRing.closed_field_axiom [definition, in mathcomp.algebra.ssralg]
GRing.ComAlgExports [module, in mathcomp.algebra.ssralg]
[ comAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.comm [definition, in mathcomp.algebra.ssralg]
GRing.commrB [lemma, in mathcomp.algebra.ssralg]
GRing.commrD [lemma, in mathcomp.algebra.ssralg]
GRing.commrM [lemma, in mathcomp.algebra.ssralg]
GRing.commrMn [lemma, in mathcomp.algebra.ssralg]
GRing.commrN [lemma, in mathcomp.algebra.ssralg]
GRing.commrN1 [lemma, in mathcomp.algebra.ssralg]
GRing.commrV [lemma, in mathcomp.algebra.ssralg]
GRing.commrX [lemma, in mathcomp.algebra.ssralg]
GRing.commr_sign [lemma, in mathcomp.algebra.ssralg]
GRing.commr_nat [lemma, in mathcomp.algebra.ssralg]
GRing.commr_prod [lemma, in mathcomp.algebra.ssralg]
GRing.commr_sum [lemma, in mathcomp.algebra.ssralg]
GRing.commr_refl [lemma, in mathcomp.algebra.ssralg]
GRing.commr_sym [lemma, in mathcomp.algebra.ssralg]
GRing.commr0 [lemma, in mathcomp.algebra.ssralg]
GRing.commr1 [lemma, in mathcomp.algebra.ssralg]
GRing.comm_alg [lemma, in mathcomp.algebra.ssralg]
GRing.comp_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.comp_is_multiplicative [lemma, in mathcomp.algebra.ssralg]
GRing.comp_is_semi_additive [lemma, in mathcomp.algebra.ssralg]
GRing.ComRingExports [module, in mathcomp.algebra.ssralg]
[ comRingType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ comRingType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.comRingMixin [lemma, in mathcomp.algebra.ssralg]
GRing.ComRingTheory [section, in mathcomp.algebra.ssralg]
GRing.ComRingTheory.FrobeniusAutomorphism [section, in mathcomp.algebra.ssralg]
GRing.ComRingTheory.FrobeniusAutomorphism.charRp [variable, in mathcomp.algebra.ssralg]
GRing.ComRingTheory.FrobeniusAutomorphism.p [variable, in mathcomp.algebra.ssralg]
GRing.ComRingTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.ComRingTheory.ScaleLinear [section, in mathcomp.algebra.ssralg]
GRing.ComRingTheory.ScaleLinear.b [variable, in mathcomp.algebra.ssralg]
GRing.ComRingTheory.ScaleLinear.f [variable, in mathcomp.algebra.ssralg]
GRing.ComRingTheory.ScaleLinear.U [variable, in mathcomp.algebra.ssralg]
GRing.ComRingTheory.ScaleLinear.V [variable, in mathcomp.algebra.ssralg]
GRing.ComSemiRingExports [module, in mathcomp.algebra.ssralg]
[ comSemiRingType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ comSemiRingType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.ComSemiRingTheory [section, in mathcomp.algebra.ssralg]
GRing.ComSemiRingTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.ComUnitAlgebraExports [module, in mathcomp.algebra.ssralg]
[ comUnitAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.ComUnitRingExports [module, in mathcomp.algebra.ssralg]
[ comUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.ComUnitRingTheory [section, in mathcomp.algebra.ssralg]
GRing.ComUnitRingTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.Const [constructor, in mathcomp.algebra.ssralg]
GRing.converse [definition, in mathcomp.algebra.ssralg]
GRing.ConverseRingExports [module, in mathcomp.algebra.ssralg]
GRing.DecFieldExports [module, in mathcomp.algebra.ssralg]
[ decFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ decFieldType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.DecidableFieldTheory [section, in mathcomp.algebra.ssralg]
GRing.DecidableFieldTheory.F [variable, in mathcomp.algebra.ssralg]
GRing.decidable_field_axiom [definition, in mathcomp.algebra.ssralg]
GRing.divalg_closedZ [lemma, in mathcomp.algebra.ssralg]
GRing.divalg_closedBdiv [lemma, in mathcomp.algebra.ssralg]
GRing.divalg_closed [definition, in mathcomp.algebra.ssralg]
GRing.divff [lemma, in mathcomp.algebra.ssralg]
GRing.divfI [lemma, in mathcomp.algebra.ssralg]
GRing.divfK [definition, in mathcomp.algebra.ssralg]
GRing.divIf [lemma, in mathcomp.algebra.ssralg]
GRing.divIr [lemma, in mathcomp.algebra.ssralg]
GRing.divKf [lemma, in mathcomp.algebra.ssralg]
GRing.divKr [lemma, in mathcomp.algebra.ssralg]
GRing.divrI [lemma, in mathcomp.algebra.ssralg]
GRing.divringClosedP [lemma, in mathcomp.algebra.ssralg]
GRing.divring_closed_div [lemma, in mathcomp.algebra.ssralg]
GRing.divring_closedBM [lemma, in mathcomp.algebra.ssralg]
GRing.divring_closed [definition, in mathcomp.algebra.ssralg]
GRing.divrK [definition, in mathcomp.algebra.ssralg]
GRing.divrN [lemma, in mathcomp.algebra.ssralg]
GRing.divrNN [lemma, in mathcomp.algebra.ssralg]
GRing.divrr [lemma, in mathcomp.algebra.ssralg]
GRing.divr_signM [lemma, in mathcomp.algebra.ssralg]
GRing.divr_closedM [lemma, in mathcomp.algebra.ssralg]
GRing.divr_closedV [lemma, in mathcomp.algebra.ssralg]
GRing.divr_closed [definition, in mathcomp.algebra.ssralg]
GRing.divr_2closed [definition, in mathcomp.algebra.ssralg]
GRing.divr1 [lemma, in mathcomp.algebra.ssralg]
GRing.divr1_eq [lemma, in mathcomp.algebra.ssralg]
GRing.div1r [lemma, in mathcomp.algebra.ssralg]
GRing.dnf_to_rform [lemma, in mathcomp.algebra.ssralg]
GRing.dnf_rterm [definition, in mathcomp.algebra.ssralg]
GRing.dnf_to_form_qf [lemma, in mathcomp.algebra.ssralg]
GRing.dnf_to_form [definition, in mathcomp.algebra.ssralg]
GRing.dvdn_charf [lemma, in mathcomp.algebra.ssralg]
GRing.eqf_sqr [lemma, in mathcomp.algebra.ssralg]
GRing.eqr_sum_div [lemma, in mathcomp.algebra.ssralg]
GRing.eqr_div [lemma, in mathcomp.algebra.ssralg]
GRing.eqr_oppLR [lemma, in mathcomp.algebra.ssralg]
GRing.eqr_opp [lemma, in mathcomp.algebra.ssralg]
GRing.Equal [constructor, in mathcomp.algebra.ssralg]
GRing.eq_sol [lemma, in mathcomp.algebra.ssralg]
GRing.eq_sat [lemma, in mathcomp.algebra.ssralg]
GRing.eq_holds [lemma, in mathcomp.algebra.ssralg]
GRing.eq_eval [lemma, in mathcomp.algebra.ssralg]
GRing.eq0_rform [definition, in mathcomp.algebra.ssralg]
GRing.eval [definition, in mathcomp.algebra.ssralg]
GRing.EvalTerm [section, in mathcomp.algebra.ssralg]
GRing.EvalTerm.If [section, in mathcomp.algebra.ssralg]
GRing.EvalTerm.If.else_f [variable, in mathcomp.algebra.ssralg]
GRing.EvalTerm.If.pred_f [variable, in mathcomp.algebra.ssralg]
GRing.EvalTerm.If.then_f [variable, in mathcomp.algebra.ssralg]
GRing.EvalTerm.MultiQuant [section, in mathcomp.algebra.ssralg]
GRing.EvalTerm.MultiQuant.f [variable, in mathcomp.algebra.ssralg]
GRing.EvalTerm.Pick [section, in mathcomp.algebra.ssralg]
GRing.EvalTerm.Pick.else_f [variable, in mathcomp.algebra.ssralg]
GRing.EvalTerm.Pick.I [variable, in mathcomp.algebra.ssralg]
GRing.EvalTerm.Pick.pred_f [variable, in mathcomp.algebra.ssralg]
GRing.EvalTerm.Pick.then_f [variable, in mathcomp.algebra.ssralg]
GRing.EvalTerm.R [variable, in mathcomp.algebra.ssralg]
[ rec _ , _ ] [notation, in mathcomp.algebra.ssralg]
GRing.eval_Pick [lemma, in mathcomp.algebra.ssralg]
GRing.eval_If [lemma, in mathcomp.algebra.ssralg]
GRing.eval_tsubst [lemma, in mathcomp.algebra.ssralg]
GRing.Exists [constructor, in mathcomp.algebra.ssralg]
GRing.Exp [constructor, in mathcomp.algebra.ssralg]
GRing.exp [definition, in mathcomp.algebra.ssralg]
GRing.expfB [lemma, in mathcomp.algebra.ssralg]
GRing.expfB_cond [lemma, in mathcomp.algebra.ssralg]
GRing.expfS_eq1 [lemma, in mathcomp.algebra.ssralg]
GRing.expf_neq0 [lemma, in mathcomp.algebra.ssralg]
GRing.expf_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.exprAC [lemma, in mathcomp.algebra.ssralg]
GRing.exprB [lemma, in mathcomp.algebra.ssralg]
GRing.exprBn [lemma, in mathcomp.algebra.ssralg]
GRing.exprBn_comm [lemma, in mathcomp.algebra.ssralg]
GRing.exprD [lemma, in mathcomp.algebra.ssralg]
GRing.exprDn [lemma, in mathcomp.algebra.ssralg]
GRing.exprDn_char [lemma, in mathcomp.algebra.ssralg]
GRing.exprDn_comm [lemma, in mathcomp.algebra.ssralg]
GRing.exprD1n [lemma, in mathcomp.algebra.ssralg]
GRing.exprM [lemma, in mathcomp.algebra.ssralg]
GRing.exprMn [lemma, in mathcomp.algebra.ssralg]
GRing.exprMn_n [lemma, in mathcomp.algebra.ssralg]
GRing.exprMn_comm [lemma, in mathcomp.algebra.ssralg]
GRing.exprNn [lemma, in mathcomp.algebra.ssralg]
GRing.exprNn_char [lemma, in mathcomp.algebra.ssralg]
GRing.exprS [lemma, in mathcomp.algebra.ssralg]
GRing.exprSr [lemma, in mathcomp.algebra.ssralg]
GRing.exprVn [lemma, in mathcomp.algebra.ssralg]
GRing.exprZn [lemma, in mathcomp.algebra.ssralg]
GRing.expr_div_n [lemma, in mathcomp.algebra.ssralg]
GRing.expr_dvd [lemma, in mathcomp.algebra.ssralg]
GRing.expr_mod [lemma, in mathcomp.algebra.ssralg]
GRing.expr_sum [lemma, in mathcomp.algebra.ssralg]
GRing.expr0 [lemma, in mathcomp.algebra.ssralg]
GRing.expr0n [lemma, in mathcomp.algebra.ssralg]
GRing.expr1 [lemma, in mathcomp.algebra.ssralg]
GRing.expr1n [lemma, in mathcomp.algebra.ssralg]
GRing.expr2 [lemma, in mathcomp.algebra.ssralg]
GRing.False [abbreviation, in mathcomp.algebra.ssralg]
GRing.fE [abbreviation, in mathcomp.algebra.ssralg]
GRing.FieldExports [module, in mathcomp.algebra.ssralg]
[ fieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ fieldType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.FieldPred [section, in mathcomp.algebra.ssralg]
GRing.FieldPred.F [variable, in mathcomp.algebra.ssralg]
GRing.FieldPred.ModuleTheory [section, in mathcomp.algebra.ssralg]
GRing.FieldPred.ModuleTheory.V [variable, in mathcomp.algebra.ssralg]
GRing.FieldPred.Predicates [section, in mathcomp.algebra.ssralg]
GRing.FieldTheory [section, in mathcomp.algebra.ssralg]
GRing.FieldTheory.F [variable, in mathcomp.algebra.ssralg]
GRing.FieldTheory.FieldMorphismInj [section, in mathcomp.algebra.ssralg]
GRing.FieldTheory.FieldMorphismInj.f [variable, in mathcomp.algebra.ssralg]
GRing.FieldTheory.FieldMorphismInj.R [variable, in mathcomp.algebra.ssralg]
GRing.FieldTheory.FieldMorphismInv [section, in mathcomp.algebra.ssralg]
GRing.FieldTheory.FieldMorphismInv.f [variable, in mathcomp.algebra.ssralg]
GRing.FieldTheory.FieldMorphismInv.R [variable, in mathcomp.algebra.ssralg]
GRing.FieldTheory.ModuleTheory [section, in mathcomp.algebra.ssralg]
GRing.FieldTheory.ModuleTheory.V [variable, in mathcomp.algebra.ssralg]
GRing.field_axiom [definition, in mathcomp.algebra.ssralg]
GRing.fmorphV [lemma, in mathcomp.algebra.ssralg]
GRing.fmorph_div [lemma, in mathcomp.algebra.ssralg]
GRing.fmorph_unit [lemma, in mathcomp.algebra.ssralg]
GRing.fmorph_char [lemma, in mathcomp.algebra.ssralg]
GRing.fmorph_eq1 [lemma, in mathcomp.algebra.ssralg]
GRing.fmorph_eq [lemma, in mathcomp.algebra.ssralg]
GRing.fmorph_inj [lemma, in mathcomp.algebra.ssralg]
GRing.fmorph_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.foldExistsP [lemma, in mathcomp.algebra.ssralg]
GRing.foldForallP [lemma, in mathcomp.algebra.ssralg]
GRing.Forall [constructor, in mathcomp.algebra.ssralg]
GRing.formula [inductive, in mathcomp.algebra.ssralg]
GRing.fpredMl [lemma, in mathcomp.algebra.ssralg]
GRing.fpredMr [lemma, in mathcomp.algebra.ssralg]
GRing.fpred_divr [lemma, in mathcomp.algebra.ssralg]
GRing.fpred_divl [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_aut_is_multiplicative [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_aut_is_additive [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_autB_comm [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_autN [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_autX [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_autM_comm [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_aut_nat [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_autMn [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_autD_comm [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_aut1 [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_aut0 [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_autE [lemma, in mathcomp.algebra.ssralg]
GRing.Frobenius_aut [definition, in mathcomp.algebra.ssralg]
GRing.fsubst [definition, in mathcomp.algebra.ssralg]
GRing.holds [definition, in mathcomp.algebra.ssralg]
GRing.holds_fsubst [lemma, in mathcomp.algebra.ssralg]
GRing.idfun_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.idfun_is_multiplicative [lemma, in mathcomp.algebra.ssralg]
GRing.idfun_is_semi_additive [lemma, in mathcomp.algebra.ssralg]
GRing.IdomainMixin [lemma, in mathcomp.algebra.ssralg]
GRing.If [definition, in mathcomp.algebra.ssralg]
GRing.If_form_rf [lemma, in mathcomp.algebra.ssralg]
GRing.If_form_qf [lemma, in mathcomp.algebra.ssralg]
GRing.imaginary_exists [lemma, in mathcomp.algebra.ssralg]
GRing.Implies [constructor, in mathcomp.algebra.ssralg]
GRing.IntegralDomainExports [module, in mathcomp.algebra.ssralg]
[ idomainType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ idomainType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.IntegralDomainTheory [section, in mathcomp.algebra.ssralg]
GRing.IntegralDomainTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.integral_domain_axiom [definition, in mathcomp.algebra.ssralg]
GRing.Inv [constructor, in mathcomp.algebra.ssralg]
GRing.invfM [lemma, in mathcomp.algebra.ssralg]
GRing.invf_div [lemma, in mathcomp.algebra.ssralg]
GRing.invrK [lemma, in mathcomp.algebra.ssralg]
GRing.invrM [lemma, in mathcomp.algebra.ssralg]
GRing.invrN [lemma, in mathcomp.algebra.ssralg]
GRing.invrN1 [lemma, in mathcomp.algebra.ssralg]
GRing.invrZ [lemma, in mathcomp.algebra.ssralg]
GRing.invr_signM [lemma, in mathcomp.algebra.ssralg]
GRing.invr_closed [definition, in mathcomp.algebra.ssralg]
GRing.invr_eq1 [lemma, in mathcomp.algebra.ssralg]
GRing.invr_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.invr_neq0 [lemma, in mathcomp.algebra.ssralg]
GRing.invr_sign [lemma, in mathcomp.algebra.ssralg]
GRing.invr_inj [lemma, in mathcomp.algebra.ssralg]
GRing.invr_out [lemma, in mathcomp.algebra.ssralg]
GRing.invr0 [lemma, in mathcomp.algebra.ssralg]
GRing.invr1 [lemma, in mathcomp.algebra.ssralg]
GRing.in_alg [abbreviation, in mathcomp.algebra.ssralg]
GRing.in_algE [lemma, in mathcomp.algebra.ssralg]
GRing.in_alg_is_rmorphism [lemma, in mathcomp.algebra.ssralg]
GRing.in_alg_is_additive [lemma, in mathcomp.algebra.ssralg]
GRing.in_alg_loc [abbreviation, in mathcomp.algebra.ssralg]
GRing.in_alg_head [definition, in mathcomp.algebra.ssralg]
GRing.iter_mulr_1 [lemma, in mathcomp.algebra.ssralg]
GRing.iter_mulr [lemma, in mathcomp.algebra.ssralg]
GRing.iter_addr_0 [lemma, in mathcomp.algebra.ssralg]
GRing.iter_addr [lemma, in mathcomp.algebra.ssralg]
GRing.LalgebraTheory [section, in mathcomp.algebra.ssralg]
GRing.LalgebraTheory.A [variable, in mathcomp.algebra.ssralg]
GRing.LalgebraTheory.ClosedPredicates [section, in mathcomp.algebra.ssralg]
GRing.LalgebraTheory.ClosedPredicates.S [variable, in mathcomp.algebra.ssralg]
GRing.LalgebraTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.LalgExports [module, in mathcomp.algebra.ssralg]
[ lalgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ lalgType _ of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.lalgMixin [lemma, in mathcomp.algebra.ssralg]
GRing.LalgPred [section, in mathcomp.algebra.ssralg]
GRing.LalgPred.A [variable, in mathcomp.algebra.ssralg]
GRing.LalgPred.R [variable, in mathcomp.algebra.ssralg]
GRing.lastr_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.LiftedNmod [section, in mathcomp.algebra.ssralg]
GRing.LiftedNmod.U [variable, in mathcomp.algebra.ssralg]
GRing.LiftedNmod.V [variable, in mathcomp.algebra.ssralg]
GRing.LiftedScale [section, in mathcomp.algebra.ssralg]
GRing.LiftedScale.A [variable, in mathcomp.algebra.ssralg]
GRing.LiftedScale.R [variable, in mathcomp.algebra.ssralg]
GRing.LiftedScale.U [variable, in mathcomp.algebra.ssralg]
GRing.LiftedScale.V [variable, in mathcomp.algebra.ssralg]
GRing.LiftedSemiRing [section, in mathcomp.algebra.ssralg]
GRing.LiftedSemiRing.R [variable, in mathcomp.algebra.ssralg]
GRing.LiftedSemiRing.T [variable, in mathcomp.algebra.ssralg]
GRing.LiftedZmod [section, in mathcomp.algebra.ssralg]
GRing.LiftedZmod.U [variable, in mathcomp.algebra.ssralg]
GRing.LiftedZmod.V [variable, in mathcomp.algebra.ssralg]
GRing.linear [section, in mathcomp.algebra.ssralg]
GRing.linearB [lemma, in mathcomp.algebra.ssralg]
GRing.linearD [lemma, in mathcomp.algebra.ssralg]
GRing.LinearExports [module, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear [module, in mathcomp.algebra.ssralg]
GRing.LinearExports.linear [abbreviation, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.apply [abbreviation, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.apply_deprecated [definition, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.Linear [section, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.Linear.R [variable, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.Linear.s [variable, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.Linear.U [variable, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.Linear.V [variable, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.mapUV [abbreviation, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.map_for_map [projection, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.map_for [record, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.map_at [definition, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.map_class [definition, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.unify_map_at [definition, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.unwrap [projection, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.wrap [definition, in mathcomp.algebra.ssralg]
GRing.LinearExports.Linear.wrapped [record, in mathcomp.algebra.ssralg]
GRing.LinearExports.scalable [abbreviation, in mathcomp.algebra.ssralg]
GRing.LinearExports.scalar [abbreviation, in mathcomp.algebra.ssralg]
[ linear of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ linear of _ as _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
{ scalar _ } (type_scope) [notation, in mathcomp.algebra.ssralg]
{ linear _ -> _ } (type_scope) [notation, in mathcomp.algebra.ssralg]
{ linear _ -> _ | _ } (type_scope) [notation, in mathcomp.algebra.ssralg]
GRing.linearMn [lemma, in mathcomp.algebra.ssralg]
GRing.linearMNn [lemma, in mathcomp.algebra.ssralg]
GRing.linearN [lemma, in mathcomp.algebra.ssralg]
GRing.linearP [lemma, in mathcomp.algebra.ssralg]
GRing.linearPZ [lemma, in mathcomp.algebra.ssralg]
GRing.LinearTheory [section, in mathcomp.algebra.ssralg]
GRing.LinearTheory.BidirectionalLinearZ [section, in mathcomp.algebra.ssralg]
GRing.LinearTheory.BidirectionalLinearZ.h [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.BidirectionalLinearZ.S [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.BidirectionalLinearZ.s [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.BidirectionalLinearZ.U [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.BidirectionalLinearZ.V [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.GenericProperties [section, in mathcomp.algebra.ssralg]
GRing.LinearTheory.GenericProperties.f [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.GenericProperties.k [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.GenericProperties.s [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.GenericProperties.U [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.GenericProperties.V [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLalg [section, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLalg.a [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLalg.A [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLalg.f [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLalg.U [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod [section, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.Plain [section, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.Plain.f [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.Plain.h [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.Plain.s [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.Scale [section, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.Scale.f [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.Scale.g [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.Scale.s [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.U [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.V [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LinearLmod.W [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LmodProperties [section, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LmodProperties.f [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LmodProperties.U [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.LmodProperties.V [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.ScalarProperties [section, in mathcomp.algebra.ssralg]
GRing.LinearTheory.ScalarProperties.f [variable, in mathcomp.algebra.ssralg]
GRing.LinearTheory.ScalarProperties.U [variable, in mathcomp.algebra.ssralg]
GRing.linearZ [lemma, in mathcomp.algebra.ssralg]
GRing.linearZZ [lemma, in mathcomp.algebra.ssralg]
GRing.linearZ_LR [lemma, in mathcomp.algebra.ssralg]
GRing.linear_sum [lemma, in mathcomp.algebra.ssralg]
GRing.linear_for [definition, in mathcomp.algebra.ssralg]
GRing.linear_closedB [lemma, in mathcomp.algebra.ssralg]
GRing.linear_closed [definition, in mathcomp.algebra.ssralg]
GRing.linear0 [lemma, in mathcomp.algebra.ssralg]
GRing.LmodExports [module, in mathcomp.algebra.ssralg]
[ lmodType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ lmodType _ of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.LmodPred [section, in mathcomp.algebra.ssralg]
GRing.LmodPred.R [variable, in mathcomp.algebra.ssralg]
GRing.LmodPred.V [variable, in mathcomp.algebra.ssralg]
GRing.LmoduleTheory [section, in mathcomp.algebra.ssralg]
GRing.LmoduleTheory.ClosedPredicates [section, in mathcomp.algebra.ssralg]
GRing.LmoduleTheory.ClosedPredicates.S [variable, in mathcomp.algebra.ssralg]
GRing.LmoduleTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.LmoduleTheory.V [variable, in mathcomp.algebra.ssralg]
GRing.lreg [definition, in mathcomp.algebra.ssralg]
GRing.lregM [lemma, in mathcomp.algebra.ssralg]
GRing.lregMl [lemma, in mathcomp.algebra.ssralg]
GRing.lregN [lemma, in mathcomp.algebra.ssralg]
GRing.lregP [lemma, in mathcomp.algebra.ssralg]
GRing.lregX [lemma, in mathcomp.algebra.ssralg]
GRing.lreg_sign [lemma, in mathcomp.algebra.ssralg]
GRing.lreg_neq0 [lemma, in mathcomp.algebra.ssralg]
GRing.lreg1 [lemma, in mathcomp.algebra.ssralg]
GRing.LRMorphismExports [module, in mathcomp.algebra.ssralg]
GRing.LRMorphismExports.LRMorphism [module, in mathcomp.algebra.ssralg]
GRing.LRMorphismExports.LRMorphism.apply [abbreviation, in mathcomp.algebra.ssralg]
GRing.LRMorphismExports.LRMorphism.apply_deprecated [definition, in mathcomp.algebra.ssralg]
[ lrmorphism of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
{ lrmorphism _ -> _ } (type_scope) [notation, in mathcomp.algebra.ssralg]
{ lrmorphism _ -> _ | _ } (type_scope) [notation, in mathcomp.algebra.ssralg]
GRing.LRMorphismTheory [section, in mathcomp.algebra.ssralg]
GRing.LRMorphismTheory.A [variable, in mathcomp.algebra.ssralg]
GRing.LRMorphismTheory.B [variable, in mathcomp.algebra.ssralg]
GRing.LRMorphismTheory.C [variable, in mathcomp.algebra.ssralg]
GRing.LRMorphismTheory.f [variable, in mathcomp.algebra.ssralg]
GRing.LRMorphismTheory.g [variable, in mathcomp.algebra.ssralg]
GRing.LRMorphismTheory.k [variable, in mathcomp.algebra.ssralg]
GRing.LRMorphismTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.LRMorphismTheory.s [variable, in mathcomp.algebra.ssralg]
GRing.Mul [constructor, in mathcomp.algebra.ssralg]
GRing.mulfI [lemma, in mathcomp.algebra.ssralg]
GRing.mulfK [lemma, in mathcomp.algebra.ssralg]
GRing.mulfV [definition, in mathcomp.algebra.ssralg]
GRing.mulfVK [lemma, in mathcomp.algebra.ssralg]
GRing.mulf_div [lemma, in mathcomp.algebra.ssralg]
GRing.mulf_neq0 [lemma, in mathcomp.algebra.ssralg]
GRing.mulf_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.mulIf [lemma, in mathcomp.algebra.ssralg]
GRing.mulIr [lemma, in mathcomp.algebra.ssralg]
GRing.mulIr_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.mulIr0_rreg [lemma, in mathcomp.algebra.ssralg]
GRing.mulKf [lemma, in mathcomp.algebra.ssralg]
GRing.mulKr [lemma, in mathcomp.algebra.ssralg]
GRing.mull_fun_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.mull_fun_is_semi_additive [lemma, in mathcomp.algebra.ssralg]
GRing.mull_fun [definition, in mathcomp.algebra.ssralg]
GRing.mulNr [lemma, in mathcomp.algebra.ssralg]
GRing.mulNrn [lemma, in mathcomp.algebra.ssralg]
GRing.mulN1r [lemma, in mathcomp.algebra.ssralg]
GRing.mulrAC [lemma, in mathcomp.algebra.ssralg]
GRing.mulrACA [lemma, in mathcomp.algebra.ssralg]
GRing.mulrb [lemma, in mathcomp.algebra.ssralg]
GRing.mulrBl [lemma, in mathcomp.algebra.ssralg]
GRing.mulrBr [lemma, in mathcomp.algebra.ssralg]
GRing.mulrCA [lemma, in mathcomp.algebra.ssralg]
GRing.mulrI [lemma, in mathcomp.algebra.ssralg]
GRing.mulrI_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.mulrI0_lreg [lemma, in mathcomp.algebra.ssralg]
GRing.mulrK [lemma, in mathcomp.algebra.ssralg]
GRing.mulrN [lemma, in mathcomp.algebra.ssralg]
GRing.mulrnA [lemma, in mathcomp.algebra.ssralg]
GRing.mulrnAC [lemma, in mathcomp.algebra.ssralg]
GRing.mulrnAl [lemma, in mathcomp.algebra.ssralg]
GRing.mulrnAr [lemma, in mathcomp.algebra.ssralg]
GRing.mulrnBl [lemma, in mathcomp.algebra.ssralg]
GRing.mulrnBr [lemma, in mathcomp.algebra.ssralg]
GRing.mulrnDl [lemma, in mathcomp.algebra.ssralg]
GRing.mulrnDr [lemma, in mathcomp.algebra.ssralg]
GRing.mulrNN [lemma, in mathcomp.algebra.ssralg]
GRing.mulrn_char [lemma, in mathcomp.algebra.ssralg]
GRing.mulrN1 [lemma, in mathcomp.algebra.ssralg]
GRing.mulrS [lemma, in mathcomp.algebra.ssralg]
GRing.mulrSr [lemma, in mathcomp.algebra.ssralg]
GRing.mulrV [definition, in mathcomp.algebra.ssralg]
GRing.mulrVK [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_algr [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_fun_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_fun_is_semi_additive [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_fun [definition, in mathcomp.algebra.ssralg]
GRing.mulr_algl [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_signM [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_sign [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_closed [definition, in mathcomp.algebra.ssralg]
GRing.mulr_2closed [definition, in mathcomp.algebra.ssralg]
GRing.mulr_natr [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_natl [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_sumr [lemma, in mathcomp.algebra.ssralg]
GRing.mulr_suml [lemma, in mathcomp.algebra.ssralg]
GRing.mulr0n [lemma, in mathcomp.algebra.ssralg]
GRing.mulr1n [lemma, in mathcomp.algebra.ssralg]
GRing.mulr1_eq [lemma, in mathcomp.algebra.ssralg]
GRing.mulr2n [lemma, in mathcomp.algebra.ssralg]
GRing.multiplicative [section, in mathcomp.algebra.ssralg]
GRing.multiplicative [definition, in mathcomp.algebra.ssralg]
GRing.mulVf [lemma, in mathcomp.algebra.ssralg]
GRing.mulVKf [lemma, in mathcomp.algebra.ssralg]
GRing.mulVKr [lemma, in mathcomp.algebra.ssralg]
GRing.mulVr [lemma, in mathcomp.algebra.ssralg]
GRing.mul_fun [definition, in mathcomp.algebra.ssralg]
GRing.mul0rn [lemma, in mathcomp.algebra.ssralg]
GRing.NatConst [constructor, in mathcomp.algebra.ssralg]
GRing.natf_neq0 [lemma, in mathcomp.algebra.ssralg]
GRing.natf0_char [lemma, in mathcomp.algebra.ssralg]
GRing.NatMul [constructor, in mathcomp.algebra.ssralg]
GRing.natmul [definition, in mathcomp.algebra.ssralg]
GRing.natrB [lemma, in mathcomp.algebra.ssralg]
GRing.natrD [lemma, in mathcomp.algebra.ssralg]
GRing.natrM [lemma, in mathcomp.algebra.ssralg]
GRing.natrX [lemma, in mathcomp.algebra.ssralg]
GRing.natr_div [lemma, in mathcomp.algebra.ssralg]
GRing.natr_mod_char [lemma, in mathcomp.algebra.ssralg]
GRing.natr_prod [lemma, in mathcomp.algebra.ssralg]
GRing.natr_sum [definition, in mathcomp.algebra.ssralg]
GRing.natr1 [lemma, in mathcomp.algebra.ssralg]
GRing.nat1r [lemma, in mathcomp.algebra.ssralg]
GRing.NmodExports [module, in mathcomp.algebra.ssralg]
[ nmodType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ nmodType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.NmodulePred [section, in mathcomp.algebra.ssralg]
GRing.NmodulePred.Add [section, in mathcomp.algebra.ssralg]
GRing.NmodulePred.Add.S [variable, in mathcomp.algebra.ssralg]
GRing.NmodulePred.V [variable, in mathcomp.algebra.ssralg]
GRing.NmoduleTheory [section, in mathcomp.algebra.ssralg]
GRing.NmoduleTheory.ClosedPredicates [section, in mathcomp.algebra.ssralg]
GRing.NmoduleTheory.ClosedPredicates.S [variable, in mathcomp.algebra.ssralg]
GRing.NmoduleTheory.V [variable, in mathcomp.algebra.ssralg]
GRing.Not [constructor, in mathcomp.algebra.ssralg]
GRing.null_fun_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.null_fun_is_semi_additive [lemma, in mathcomp.algebra.ssralg]
GRing.null_fun [definition, in mathcomp.algebra.ssralg]
GRing.oner_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.Opp [constructor, in mathcomp.algebra.ssralg]
GRing.opprB [lemma, in mathcomp.algebra.ssralg]
GRing.opprD [lemma, in mathcomp.algebra.ssralg]
GRing.opprK [lemma, in mathcomp.algebra.ssralg]
GRing.oppr_char2 [lemma, in mathcomp.algebra.ssralg]
GRing.oppr_closed [definition, in mathcomp.algebra.ssralg]
GRing.oppr_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.oppr_inj [lemma, in mathcomp.algebra.ssralg]
GRing.oppr0 [lemma, in mathcomp.algebra.ssralg]
GRing.opp_fun_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.opp_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.opp_fun_is_additive [lemma, in mathcomp.algebra.ssralg]
GRing.opp_is_additive [lemma, in mathcomp.algebra.ssralg]
GRing.opp_fun [definition, in mathcomp.algebra.ssralg]
GRing.Or [constructor, in mathcomp.algebra.ssralg]
GRing.Pick [definition, in mathcomp.algebra.ssralg]
GRing.Pick_form_qf [lemma, in mathcomp.algebra.ssralg]
GRing.prodfV [lemma, in mathcomp.algebra.ssralg]
GRing.prodf_div [lemma, in mathcomp.algebra.ssralg]
GRing.prodf_seq_neq0 [lemma, in mathcomp.algebra.ssralg]
GRing.prodf_neq0 [lemma, in mathcomp.algebra.ssralg]
GRing.prodf_seq_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.prodf_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.prodrMn [lemma, in mathcomp.algebra.ssralg]
GRing.prodrMn_const [lemma, in mathcomp.algebra.ssralg]
GRing.prodrN [lemma, in mathcomp.algebra.ssralg]
GRing.prodrXl [lemma, in mathcomp.algebra.ssralg]
GRing.prodrXr [lemma, in mathcomp.algebra.ssralg]
GRing.prodr_undup_exp_count [lemma, in mathcomp.algebra.ssralg]
GRing.prodr_const_nat [lemma, in mathcomp.algebra.ssralg]
GRing.prodr_const [lemma, in mathcomp.algebra.ssralg]
GRing.proj_satP [lemma, in mathcomp.algebra.ssralg]
GRing.proj_sat [definition, in mathcomp.algebra.ssralg]
GRing.QE_Mixin.elim_aux [variable, in mathcomp.algebra.ssralg]
GRing.QE_Mixin.ok_proj [variable, in mathcomp.algebra.ssralg]
GRing.QE_Mixin.wf_proj [variable, in mathcomp.algebra.ssralg]
GRing.QE_Mixin.proj [variable, in mathcomp.algebra.ssralg]
GRing.QE_Mixin.F [variable, in mathcomp.algebra.ssralg]
GRing.QE_Mixin [section, in mathcomp.algebra.ssralg]
GRing.qf_to_dnf_rterm [lemma, in mathcomp.algebra.ssralg]
GRing.qf_to_dnfP [lemma, in mathcomp.algebra.ssralg]
GRing.qf_to_dnf [definition, in mathcomp.algebra.ssralg]
GRing.qf_evalP [lemma, in mathcomp.algebra.ssralg]
GRing.qf_eval [definition, in mathcomp.algebra.ssralg]
GRing.qf_form [definition, in mathcomp.algebra.ssralg]
GRing.quantifier_elim_rformP [lemma, in mathcomp.algebra.ssralg]
GRing.quantifier_elim_wf [lemma, in mathcomp.algebra.ssralg]
GRing.quantifier_elim [definition, in mathcomp.algebra.ssralg]
GRing.raddfB [lemma, in mathcomp.algebra.ssralg]
GRing.raddfD [lemma, in mathcomp.algebra.ssralg]
GRing.raddfMn [lemma, in mathcomp.algebra.ssralg]
GRing.raddfMnat [lemma, in mathcomp.algebra.ssralg]
GRing.raddfMNn [lemma, in mathcomp.algebra.ssralg]
GRing.raddfMsign [lemma, in mathcomp.algebra.ssralg]
GRing.raddfN [lemma, in mathcomp.algebra.ssralg]
GRing.raddfZnat [lemma, in mathcomp.algebra.ssralg]
GRing.raddfZsign [lemma, in mathcomp.algebra.ssralg]
GRing.raddf_inj [lemma, in mathcomp.algebra.ssralg]
GRing.raddf_sum [lemma, in mathcomp.algebra.ssralg]
GRing.raddf_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.raddf0 [lemma, in mathcomp.algebra.ssralg]
GRing.regular [definition, in mathcomp.algebra.ssralg]
GRing.RegularConverseComUnitRingExports [module, in mathcomp.algebra.ssralg]
GRing.RegularConverseComUnitRingExports.ComUnitRingTheory [section, in mathcomp.algebra.ssralg]
GRing.RegularConverseComUnitRingExports.ComUnitRingTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.RegularConverseUnitRingExports [module, in mathcomp.algebra.ssralg]
GRing.RegularConverseUnitRingExports.UnitRingTheory [section, in mathcomp.algebra.ssralg]
GRing.RegularConverseUnitRingExports.UnitRingTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.RegularIdomainExports [module, in mathcomp.algebra.ssralg]
GRing.RegularLalgExports [module, in mathcomp.algebra.ssralg]
GRing.RegularLalgExports.LalgebraTheory [section, in mathcomp.algebra.ssralg]
GRing.RegularLalgExports.LalgebraTheory.A [variable, in mathcomp.algebra.ssralg]
GRing.RegularLalgExports.LalgebraTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.revrX [lemma, in mathcomp.algebra.ssralg]
GRing.rev_unitrP [lemma, in mathcomp.algebra.ssralg]
GRing.rformula [definition, in mathcomp.algebra.ssralg]
GRing.RightRegular [section, in mathcomp.algebra.ssralg]
GRing.RightRegular.R [variable, in mathcomp.algebra.ssralg]
GRing.RingExports [module, in mathcomp.algebra.ssralg]
[ ringType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ ringType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.RingPred [section, in mathcomp.algebra.ssralg]
GRing.RingPred.R [variable, in mathcomp.algebra.ssralg]
GRing.RingTheory [section, in mathcomp.algebra.ssralg]
GRing.RingTheory.Char2 [section, in mathcomp.algebra.ssralg]
GRing.RingTheory.Char2.charR2 [variable, in mathcomp.algebra.ssralg]
GRing.RingTheory.ClosedPredicates [section, in mathcomp.algebra.ssralg]
GRing.RingTheory.ClosedPredicates.S [variable, in mathcomp.algebra.ssralg]
GRing.RingTheory.FrobeniusAutomorphism [section, in mathcomp.algebra.ssralg]
GRing.RingTheory.FrobeniusAutomorphism.charFp [variable, in mathcomp.algebra.ssralg]
GRing.RingTheory.FrobeniusAutomorphism.p [variable, in mathcomp.algebra.ssralg]
_ ^f [notation, in mathcomp.algebra.ssralg]
GRing.RingTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.rmorphB [lemma, in mathcomp.algebra.ssralg]
GRing.rmorphD [lemma, in mathcomp.algebra.ssralg]
GRing.RMorphismExports [module, in mathcomp.algebra.ssralg]
[ rmorphism of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ rmorphism of _ as _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
{ rmorphism _ -> _ } (type_scope) [notation, in mathcomp.algebra.ssralg]
GRing.rmorphismMP [lemma, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory [section, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.InAlgebra [section, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.InAlgebra.A [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.InAlgebra.R [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Projections [section, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Projections.f [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Projections.g [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Projections.R [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Projections.S [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Projections.T [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties [section, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties [section, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties.f [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties.f [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties.k [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties.k [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties.R [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties.R [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties.S [variable, in mathcomp.algebra.ssralg]
GRing.RmorphismTheory.Properties.S [variable, in mathcomp.algebra.ssralg]
GRing.rmorphM [lemma, in mathcomp.algebra.ssralg]
GRing.rmorphMn [lemma, in mathcomp.algebra.ssralg]
GRing.rmorphMNn [lemma, in mathcomp.algebra.ssralg]
GRing.rmorphMsign [lemma, in mathcomp.algebra.ssralg]
GRing.rmorphN [lemma, in mathcomp.algebra.ssralg]
GRing.rmorphN1 [lemma, in mathcomp.algebra.ssralg]
GRing.rmorphV [lemma, in mathcomp.algebra.ssralg]
GRing.rmorphXn [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_div [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_unit [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_comm [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_alg [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_sign [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_eq1 [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_eq_nat [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_char [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_nat [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_prod [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph_sum [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph0 [lemma, in mathcomp.algebra.ssralg]
GRing.rmorph1 [lemma, in mathcomp.algebra.ssralg]
GRing.rpredB [lemma, in mathcomp.algebra.ssralg]
GRing.rpredBC [lemma, in mathcomp.algebra.ssralg]
GRing.rpredBl [lemma, in mathcomp.algebra.ssralg]
GRing.rpredBr [lemma, in mathcomp.algebra.ssralg]
GRing.rpredD [lemma, in mathcomp.algebra.ssralg]
GRing.rpredDl [lemma, in mathcomp.algebra.ssralg]
GRing.rpredDr [lemma, in mathcomp.algebra.ssralg]
GRing.rpredMl [lemma, in mathcomp.algebra.ssralg]
GRing.rpredMn [lemma, in mathcomp.algebra.ssralg]
GRing.rpredMNn [lemma, in mathcomp.algebra.ssralg]
GRing.rpredMr [lemma, in mathcomp.algebra.ssralg]
GRing.rpredMsign [lemma, in mathcomp.algebra.ssralg]
GRing.rpredN [lemma, in mathcomp.algebra.ssralg]
GRing.rpredN1 [lemma, in mathcomp.algebra.ssralg]
GRing.rpredV [lemma, in mathcomp.algebra.ssralg]
GRing.rpredX [lemma, in mathcomp.algebra.ssralg]
GRing.rpredXN [lemma, in mathcomp.algebra.ssralg]
GRing.rpredZeq [lemma, in mathcomp.algebra.ssralg]
GRing.rpredZnat [lemma, in mathcomp.algebra.ssralg]
GRing.rpredZsign [lemma, in mathcomp.algebra.ssralg]
GRing.rpred_divl [lemma, in mathcomp.algebra.ssralg]
GRing.rpred_divr [lemma, in mathcomp.algebra.ssralg]
GRing.rpred_div [lemma, in mathcomp.algebra.ssralg]
GRing.rpred_sign [lemma, in mathcomp.algebra.ssralg]
GRing.rpred_nat [lemma, in mathcomp.algebra.ssralg]
GRing.rpred_prod [lemma, in mathcomp.algebra.ssralg]
GRing.rpred_sum [lemma, in mathcomp.algebra.ssralg]
GRing.rpred0 [lemma, in mathcomp.algebra.ssralg]
GRing.rpred1M [lemma, in mathcomp.algebra.ssralg]
GRing.rreg [definition, in mathcomp.algebra.ssralg]
GRing.rregM [lemma, in mathcomp.algebra.ssralg]
GRing.rregMr [lemma, in mathcomp.algebra.ssralg]
GRing.rregN [lemma, in mathcomp.algebra.ssralg]
GRing.rregP [lemma, in mathcomp.algebra.ssralg]
GRing.rregX [lemma, in mathcomp.algebra.ssralg]
GRing.rreg_neq0 [lemma, in mathcomp.algebra.ssralg]
GRing.rreg1 [lemma, in mathcomp.algebra.ssralg]
GRing.rterm [definition, in mathcomp.algebra.ssralg]
GRing.same_env_sym [lemma, in mathcomp.algebra.ssralg]
GRing.same_env [definition, in mathcomp.algebra.ssralg]
GRing.scalable_linear [lemma, in mathcomp.algebra.ssralg]
GRing.scalable_for [definition, in mathcomp.algebra.ssralg]
GRing.scalarP [lemma, in mathcomp.algebra.ssralg]
GRing.scalarZ [lemma, in mathcomp.algebra.ssralg]
GRing.Scale [module, in mathcomp.algebra.ssralg]
GRing.scaleNr [lemma, in mathcomp.algebra.ssralg]
GRing.scaleN1r [lemma, in mathcomp.algebra.ssralg]
GRing.scalerBl [lemma, in mathcomp.algebra.ssralg]
GRing.scalerBr [lemma, in mathcomp.algebra.ssralg]
GRing.scalerCA [lemma, in mathcomp.algebra.ssralg]
GRing.scalerI [lemma, in mathcomp.algebra.ssralg]
GRing.scalerK [lemma, in mathcomp.algebra.ssralg]
GRing.scalerKV [lemma, in mathcomp.algebra.ssralg]
GRing.scalerMnl [lemma, in mathcomp.algebra.ssralg]
GRing.scalerMnr [lemma, in mathcomp.algebra.ssralg]
GRing.scalerN [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_unit [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_injl [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_prodr [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_prodl [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_prod [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_closed [definition, in mathcomp.algebra.ssralg]
GRing.scaler_sumr [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_suml [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_sign [lemma, in mathcomp.algebra.ssralg]
GRing.scaler_nat [lemma, in mathcomp.algebra.ssralg]
GRing.scaler0 [lemma, in mathcomp.algebra.ssralg]
GRing.scale_fun_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.scale_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.scale_fun [definition, in mathcomp.algebra.ssralg]
GRing.Scale.compN1op [lemma, in mathcomp.algebra.ssralg]
GRing.Scale.Exports [module, in mathcomp.algebra.ssralg]
GRing.Scale.law [definition, in mathcomp.algebra.ssralg]
GRing.Scale.N1op [lemma, in mathcomp.algebra.ssralg]
GRing.Scale.opB [lemma, in mathcomp.algebra.ssralg]
GRing.Scale.ScaleLaw [section, in mathcomp.algebra.ssralg]
GRing.Scale.ScaleLaw.aR [variable, in mathcomp.algebra.ssralg]
GRing.Scale.ScaleLaw.nu [variable, in mathcomp.algebra.ssralg]
GRing.Scale.ScaleLaw.R [variable, in mathcomp.algebra.ssralg]
GRing.Scale.ScaleLaw.s_law [variable, in mathcomp.algebra.ssralg]
GRing.Scale.ScaleLaw.V [variable, in mathcomp.algebra.ssralg]
GRing.scale0r [lemma, in mathcomp.algebra.ssralg]
GRing.sdivr_closedM [lemma, in mathcomp.algebra.ssralg]
GRing.sdivr_closed_div [lemma, in mathcomp.algebra.ssralg]
GRing.sdivr_closed [definition, in mathcomp.algebra.ssralg]
GRing.SemiRightRegular [section, in mathcomp.algebra.ssralg]
GRing.SemiRightRegular.R [variable, in mathcomp.algebra.ssralg]
GRing.semiringClosedP [lemma, in mathcomp.algebra.ssralg]
GRing.SemiRingExports [module, in mathcomp.algebra.ssralg]
[ semiRingType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ semiRingType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.SemiRingPred [section, in mathcomp.algebra.ssralg]
GRing.SemiRingPred.Mul [section, in mathcomp.algebra.ssralg]
GRing.SemiRingPred.Mul.S [variable, in mathcomp.algebra.ssralg]
GRing.SemiRingPred.R [variable, in mathcomp.algebra.ssralg]
GRing.SemiRingTheory [section, in mathcomp.algebra.ssralg]
GRing.SemiRingTheory.Char2 [section, in mathcomp.algebra.ssralg]
GRing.SemiRingTheory.Char2.charR2 [variable, in mathcomp.algebra.ssralg]
GRing.SemiRingTheory.ClosedPredicates [section, in mathcomp.algebra.ssralg]
GRing.SemiRingTheory.ClosedPredicates.S [variable, in mathcomp.algebra.ssralg]
GRing.SemiRingTheory.FrobeniusAutomorphism [section, in mathcomp.algebra.ssralg]
GRing.SemiRingTheory.FrobeniusAutomorphism.charFp [variable, in mathcomp.algebra.ssralg]
GRing.SemiRingTheory.FrobeniusAutomorphism.p [variable, in mathcomp.algebra.ssralg]
_ ^f [notation, in mathcomp.algebra.ssralg]
GRing.SemiRingTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.semiring_closedM [lemma, in mathcomp.algebra.ssralg]
GRing.semiring_closedD [lemma, in mathcomp.algebra.ssralg]
GRing.semiring_closed [definition, in mathcomp.algebra.ssralg]
GRing.semi_additive [definition, in mathcomp.algebra.ssralg]
GRing.sign [abbreviation, in mathcomp.algebra.ssralg]
GRing.signrE [lemma, in mathcomp.algebra.ssralg]
GRing.signrMK [lemma, in mathcomp.algebra.ssralg]
GRing.signrN [lemma, in mathcomp.algebra.ssralg]
GRing.signrZK [lemma, in mathcomp.algebra.ssralg]
GRing.signr_addb [lemma, in mathcomp.algebra.ssralg]
GRing.signr_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.signr_odd [lemma, in mathcomp.algebra.ssralg]
GRing.size_sol [lemma, in mathcomp.algebra.ssralg]
GRing.smulr_closedN [lemma, in mathcomp.algebra.ssralg]
GRing.smulr_closedM [lemma, in mathcomp.algebra.ssralg]
GRing.smulr_closed [definition, in mathcomp.algebra.ssralg]
GRing.sol [definition, in mathcomp.algebra.ssralg]
GRing.solP [lemma, in mathcomp.algebra.ssralg]
GRing.sol_subproof [lemma, in mathcomp.algebra.ssralg]
GRing.sqrf_eq1 [lemma, in mathcomp.algebra.ssralg]
GRing.sqrf_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.sqrrB [lemma, in mathcomp.algebra.ssralg]
GRing.sqrrB1 [lemma, in mathcomp.algebra.ssralg]
GRing.sqrrD [lemma, in mathcomp.algebra.ssralg]
GRing.sqrrD1 [lemma, in mathcomp.algebra.ssralg]
GRing.sqrrN [lemma, in mathcomp.algebra.ssralg]
GRing.sqrr_sign [lemma, in mathcomp.algebra.ssralg]
GRing.subalgClosedP [lemma, in mathcomp.algebra.ssralg]
GRing.subalg_closedBM [lemma, in mathcomp.algebra.ssralg]
GRing.subalg_closedZ [lemma, in mathcomp.algebra.ssralg]
GRing.subalg_closed [definition, in mathcomp.algebra.ssralg]
GRing.SubExports [module, in mathcomp.algebra.ssralg]
[ SubIntegralDomain_isSubField of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubIntegralDomain of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubComUnitRing_isSubIntegralDomain of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubComUnitRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubUnitRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubRing_isSubUnitRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubAlgebra of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubLalgebra_isSubAlgebra of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubLalgebra of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubRing_SubLmodule_isSubLalgebra of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubLmodule of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubZmodule_isSubLmodule of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubComRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubRing_isSubComRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubZmodule_isSubRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubComSemiRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubSemiRing_isSubComSemiRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubSemiRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubNmodule_isSubSemiRing of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubZmodule of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ SubChoice_isSubNmodule of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.subIr [lemma, in mathcomp.algebra.ssralg]
GRing.subKr [lemma, in mathcomp.algebra.ssralg]
GRing.submodClosedP [lemma, in mathcomp.algebra.ssralg]
GRing.submod_closedZ [lemma, in mathcomp.algebra.ssralg]
GRing.submod_closedB [lemma, in mathcomp.algebra.ssralg]
GRing.submod_closed [definition, in mathcomp.algebra.ssralg]
GRing.subrI [lemma, in mathcomp.algebra.ssralg]
GRing.subringClosedP [lemma, in mathcomp.algebra.ssralg]
GRing.subring_closed_semi [lemma, in mathcomp.algebra.ssralg]
GRing.subring_closedM [lemma, in mathcomp.algebra.ssralg]
GRing.subring_closedB [lemma, in mathcomp.algebra.ssralg]
GRing.subring_closed [definition, in mathcomp.algebra.ssralg]
GRing.subrK [definition, in mathcomp.algebra.ssralg]
GRing.subrKA [lemma, in mathcomp.algebra.ssralg]
GRing.subrr [definition, in mathcomp.algebra.ssralg]
GRing.subrXX [lemma, in mathcomp.algebra.ssralg]
GRing.subrXX_comm [lemma, in mathcomp.algebra.ssralg]
GRing.subrX1 [lemma, in mathcomp.algebra.ssralg]
GRing.subr_sqrDB [lemma, in mathcomp.algebra.ssralg]
GRing.subr_sqr [lemma, in mathcomp.algebra.ssralg]
GRing.subr_char2 [lemma, in mathcomp.algebra.ssralg]
GRing.subr_sqr_1 [lemma, in mathcomp.algebra.ssralg]
GRing.subr_2closed [definition, in mathcomp.algebra.ssralg]
GRing.subr_eq0 [lemma, in mathcomp.algebra.ssralg]
GRing.subr_eq [lemma, in mathcomp.algebra.ssralg]
GRing.subr0 [lemma, in mathcomp.algebra.ssralg]
GRing.subr0_eq [lemma, in mathcomp.algebra.ssralg]
GRing.Substitution [section, in mathcomp.algebra.ssralg]
GRing.Substitution.R [variable, in mathcomp.algebra.ssralg]
GRing.sub_fun_is_scalable [lemma, in mathcomp.algebra.ssralg]
GRing.sub_fun_is_additive [lemma, in mathcomp.algebra.ssralg]
GRing.sub_fun [definition, in mathcomp.algebra.ssralg]
GRing.sub0r [lemma, in mathcomp.algebra.ssralg]
GRing.sumrB [lemma, in mathcomp.algebra.ssralg]
GRing.sumrMnl [lemma, in mathcomp.algebra.ssralg]
GRing.sumrMnr [lemma, in mathcomp.algebra.ssralg]
GRing.sumrN [lemma, in mathcomp.algebra.ssralg]
GRing.sumr_const_nat [lemma, in mathcomp.algebra.ssralg]
GRing.sumr_const [lemma, in mathcomp.algebra.ssralg]
GRing.telescope_prodf_eq [lemma, in mathcomp.algebra.ssralg]
GRing.telescope_prodf [lemma, in mathcomp.algebra.ssralg]
GRing.telescope_prodr_eq [lemma, in mathcomp.algebra.ssralg]
GRing.telescope_prodr [lemma, in mathcomp.algebra.ssralg]
GRing.telescope_sumr_eq [lemma, in mathcomp.algebra.ssralg]
GRing.telescope_sumr [lemma, in mathcomp.algebra.ssralg]
GRing.term [inductive, in mathcomp.algebra.ssralg]
GRing.TermDef [section, in mathcomp.algebra.ssralg]
GRing.TermDef.R [variable, in mathcomp.algebra.ssralg]
GRing.Theory [module, in mathcomp.algebra.ssralg]
GRing.Theory.addf_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addIr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.additive [definition, in mathcomp.algebra.ssralg]
GRing.Theory.additive_linear [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addKr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addKr_char2 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addNKr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addNr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrAC [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrACA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrC [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrCA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrI [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrKA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrK_char2 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrNK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addrr_char2 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addr_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addr0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.addr0_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.add0r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.bin_lt_charf_0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.can2_linear [definition, in mathcomp.algebra.ssralg]
GRing.Theory.can2_scalable [definition, in mathcomp.algebra.ssralg]
GRing.Theory.can2_rmorphism [definition, in mathcomp.algebra.ssralg]
GRing.Theory.can2_additive [definition, in mathcomp.algebra.ssralg]
GRing.Theory.can2_semi_additive [definition, in mathcomp.algebra.ssralg]
GRing.Theory.charf_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.charf_prime [definition, in mathcomp.algebra.ssralg]
GRing.Theory.charf'_nat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.charf0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.charf0P [definition, in mathcomp.algebra.ssralg]
GRing.Theory.char_lalg [definition, in mathcomp.algebra.ssralg]
GRing.Theory.char0_natf_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commrB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commrD [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commrM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commrMn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commrN1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commrV [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commrX [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commr_sign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commr_nat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commr_prod [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commr_sum [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commr_refl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commr_sym [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commr0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.commr1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.comm_alg [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divff [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divfI [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divfK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divIf [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divIr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divKf [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divKr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divrI [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divringClosedP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divrK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divrNN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divrr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divr_signM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divr1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.divr1_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.div1r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.dvdn_charf [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eqf_sqr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eqr_sum_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eqr_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eqr_oppLR [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eqr_opp [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eq_sol [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eq_sat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eq_holds [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eq_eval [definition, in mathcomp.algebra.ssralg]
GRing.Theory.eval_tsubst [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expfB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expfB_cond [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expfS_eq1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expf_neq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expf_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprAC [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprBn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprBn_comm [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprD [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprDn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprDn_char [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprDn_comm [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprD1n [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprMn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprMn_n [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprMn_comm [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprNn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprNn_char [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprS [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprSr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprVn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.exprZn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expr_div_n [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expr_dvd [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expr_mod [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expr_sum [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expr0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expr0n [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expr1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expr1n [definition, in mathcomp.algebra.ssralg]
GRing.Theory.expr2 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fieldP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fmorphV [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_unit [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_char [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_eq1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_inj [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fmorph_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fpredMl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fpredMr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fpred_divl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.fpred_divr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autB_comm [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autX [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autM_comm [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_aut_nat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autMn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autD_comm [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_aut1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_aut0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.Frobenius_autE [definition, in mathcomp.algebra.ssralg]
GRing.Theory.holds_fsubst [definition, in mathcomp.algebra.ssralg]
GRing.Theory.imaginary_exists [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invfM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invf_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invrK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invrM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invrN1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invrZ [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invr_signM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invr_neq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invr_eq1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invr_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invr_sign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invr_inj [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invr_out [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invr0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.invr1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.in_alg [abbreviation, in mathcomp.algebra.ssralg]
GRing.Theory.in_algE [definition, in mathcomp.algebra.ssralg]
GRing.Theory.iter_mulr_1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.iter_mulr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.iter_addr_0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.iter_addr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearD [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearE [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearMn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearMNn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearPZ [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearZ [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearZZ [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linearZ_LR [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linear_sum [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linear_for [definition, in mathcomp.algebra.ssralg]
GRing.Theory.linear0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.lregM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.lregN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.lregP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.lregX [definition, in mathcomp.algebra.ssralg]
GRing.Theory.lreg_sign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.lreg_neq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.lreg1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulfI [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulfK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulfV [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulfVK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulf_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulf_neq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulf_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulIf [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulIr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulIr_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulIr0_rreg [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulKf [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulKr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulNr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulNrn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulN1r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrAC [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrACA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrb [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrBl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrBr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrC [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrCA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrDl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrDr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrI [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrI_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrI0_lreg [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrnA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrnAC [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrnAl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrnAr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrnBl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrnBr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrnDl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrnDr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrNN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrn_char [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrN1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrS [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrSr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrV [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulrVK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr_algr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr_algl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr_signM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr_sign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr_natr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr_natl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr_sumr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr_suml [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr0n [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr1n [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr1_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulr2n [definition, in mathcomp.algebra.ssralg]
GRing.Theory.multiplicative [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulVf [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulVKf [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulVKr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mulVr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mul0r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mul0rn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.mul1r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natf_neq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natf0_char [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natrB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natrD [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natrM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natrX [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natr_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natr_prod [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natr_sum [definition, in mathcomp.algebra.ssralg]
GRing.Theory.natr1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.nat1r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.null_fun [abbreviation, in mathcomp.algebra.ssralg]
GRing.Theory.oner_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.oner_neq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.opprB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.opprD [definition, in mathcomp.algebra.ssralg]
GRing.Theory.opprK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.oppr_char2 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.oppr_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.oppr_inj [definition, in mathcomp.algebra.ssralg]
GRing.Theory.oppr0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodfV [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodf_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodf_seq_neq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodf_neq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodf_seq_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodf_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodrMn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodrMn_const [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodrXl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodrXr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodr_undup_exp_count [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodr_const_nat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.prodr_const [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddf [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddfB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddfD [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddfMn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddfMnat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddfMNn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddfMsign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddfN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddfZnat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddfZsign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddf_sum [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddf_inj [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddf_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.raddf0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.revrX [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphD [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphE [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphismMP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphMn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphMNn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphMsign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphN1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphV [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphX [abbreviation, in mathcomp.algebra.ssralg]
GRing.Theory.rmorphXn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_alg [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_unit [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_comm [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_char [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_sign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_prod [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_eq_nat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_nat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_eq1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph_sum [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rmorph1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredBC [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredBl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredBr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredD [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredDl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredDr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredMl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredMn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredMNn [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredMr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredMsign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredNr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredN1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredV [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredVr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredX [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredXN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredZ [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredZeq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredZnat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpredZsign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred_divl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred_divr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred_div [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred_sign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred_nat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred_prod [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred_sum [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred0D [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rpred1M [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rregM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rregN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rregP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rregX [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rreg_neq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.rreg1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.satP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalable_linear [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalable_for [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalarP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalarZ [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaleNr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaleN1r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerAl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerAr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerBl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerBr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerCA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerDl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerDr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerI [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerKV [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerMnl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerMnr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scalerN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_unit [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_injl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_prod [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_prodr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_prodl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_sign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_sumr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_suml [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler_nat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scaler0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scale0r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.scale1r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.semiringClosedP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.semi_additive [definition, in mathcomp.algebra.ssralg]
GRing.Theory.signrE [definition, in mathcomp.algebra.ssralg]
GRing.Theory.signrMK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.signrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.signrZK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.signr_addb [definition, in mathcomp.algebra.ssralg]
GRing.Theory.signr_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.signr_odd [definition, in mathcomp.algebra.ssralg]
GRing.Theory.size_sol [definition, in mathcomp.algebra.ssralg]
GRing.Theory.solP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.solve_monicpoly [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sqrf_eq1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sqrf_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sqrrB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sqrrB1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sqrrD [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sqrrD1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sqrrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sqrr_sign [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subalgClosedP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subIr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subKr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.submodClosedP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subrI [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subringClosedP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subrK [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subrKA [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subrr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subrXX [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subrXX_comm [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subrX1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subr_sqrDB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subr_sqr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subr_sqr_1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subr_eq0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subr_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subr0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.subr0_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sub0r [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sumrB [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sumrMnl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sumrMnr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sumrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sumr_const_nat [definition, in mathcomp.algebra.ssralg]
GRing.Theory.sumr_const [definition, in mathcomp.algebra.ssralg]
GRing.Theory.telescope_prodf_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.telescope_prodf [definition, in mathcomp.algebra.ssralg]
GRing.Theory.telescope_prodr_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.telescope_prodr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.telescope_sumr_eq [definition, in mathcomp.algebra.ssralg]
GRing.Theory.telescope_sumr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitfE [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrE [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrM [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrMl [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrMr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrM_comm [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrN [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrN1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrP [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrPr [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrV [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrX [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitrX_pos [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitr0 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.unitr1 [definition, in mathcomp.algebra.ssralg]
GRing.Theory.zmodClosedP [definition, in mathcomp.algebra.ssralg]
GRing.to_rformP [lemma, in mathcomp.algebra.ssralg]
GRing.to_rform_rformula [lemma, in mathcomp.algebra.ssralg]
GRing.to_rform [definition, in mathcomp.algebra.ssralg]
GRing.to_rterm_id [lemma, in mathcomp.algebra.ssralg]
GRing.to_rterm [definition, in mathcomp.algebra.ssralg]
GRing.True [abbreviation, in mathcomp.algebra.ssralg]
GRing.tsubst [definition, in mathcomp.algebra.ssralg]
GRing.ub_var [definition, in mathcomp.algebra.ssralg]
GRing.Unit [constructor, in mathcomp.algebra.ssralg]
GRing.unit [definition, in mathcomp.algebra.ssralg]
GRing.UnitAlgebraExports [module, in mathcomp.algebra.ssralg]
[ unitAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.UnitAlgebraTheory [section, in mathcomp.algebra.ssralg]
GRing.UnitAlgebraTheory.A [variable, in mathcomp.algebra.ssralg]
GRing.UnitAlgebraTheory.ClosedPredicates [section, in mathcomp.algebra.ssralg]
GRing.UnitAlgebraTheory.ClosedPredicates.S [variable, in mathcomp.algebra.ssralg]
GRing.UnitAlgebraTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.unitfE [lemma, in mathcomp.algebra.ssralg]
GRing.unitrE [lemma, in mathcomp.algebra.ssralg]
GRing.UnitRingClosedPredicates [section, in mathcomp.algebra.ssralg]
GRing.UnitRingClosedPredicates.R [variable, in mathcomp.algebra.ssralg]
GRing.UnitRingClosedPredicates.S [variable, in mathcomp.algebra.ssralg]
GRing.UnitRingExports [module, in mathcomp.algebra.ssralg]
[ unitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ unitRingType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.UnitRingMorphism [section, in mathcomp.algebra.ssralg]
GRing.UnitRingMorphism.f [variable, in mathcomp.algebra.ssralg]
GRing.UnitRingMorphism.R [variable, in mathcomp.algebra.ssralg]
GRing.UnitRingMorphism.S [variable, in mathcomp.algebra.ssralg]
GRing.UnitRingPred [section, in mathcomp.algebra.ssralg]
GRing.UnitRingPred.Div [section, in mathcomp.algebra.ssralg]
GRing.UnitRingPred.Div.S [variable, in mathcomp.algebra.ssralg]
GRing.UnitRingPred.R [variable, in mathcomp.algebra.ssralg]
GRing.UnitRingTheory [section, in mathcomp.algebra.ssralg]
GRing.UnitRingTheory.R [variable, in mathcomp.algebra.ssralg]
GRing.unitrM [lemma, in mathcomp.algebra.ssralg]
GRing.unitrMl [lemma, in mathcomp.algebra.ssralg]
GRing.unitrMr [lemma, in mathcomp.algebra.ssralg]
GRing.unitrM_comm [lemma, in mathcomp.algebra.ssralg]
GRing.unitrN [lemma, in mathcomp.algebra.ssralg]
GRing.unitrN1 [lemma, in mathcomp.algebra.ssralg]
GRing.unitrP [lemma, in mathcomp.algebra.ssralg]
GRing.unitrPr [lemma, in mathcomp.algebra.ssralg]
GRing.unitrV [lemma, in mathcomp.algebra.ssralg]
GRing.unitrX [lemma, in mathcomp.algebra.ssralg]
GRing.unitrX_pos [lemma, in mathcomp.algebra.ssralg]
GRing.unitr_sdivr_closed [lemma, in mathcomp.algebra.ssralg]
GRing.unitr0 [lemma, in mathcomp.algebra.ssralg]
GRing.unitr1 [lemma, in mathcomp.algebra.ssralg]
GRing.unit_pred [definition, in mathcomp.algebra.ssralg]
GRing.val [abbreviation, in mathcomp.algebra.ssralg]
GRing.val [abbreviation, in mathcomp.algebra.ssralg]
GRing.val [abbreviation, in mathcomp.algebra.ssralg]
GRing.val [abbreviation, in mathcomp.algebra.ssralg]
GRing.valB [lemma, in mathcomp.algebra.ssralg]
GRing.valD [lemma, in mathcomp.algebra.ssralg]
GRing.valid_QE_proj [definition, in mathcomp.algebra.ssralg]
GRing.valM [lemma, in mathcomp.algebra.ssralg]
GRing.valM1 [lemma, in mathcomp.algebra.ssralg]
GRing.valN [lemma, in mathcomp.algebra.ssralg]
GRing.val0 [lemma, in mathcomp.algebra.ssralg]
GRing.val1 [lemma, in mathcomp.algebra.ssralg]
GRing.Var [constructor, in mathcomp.algebra.ssralg]
GRing.wf_QE_proj [definition, in mathcomp.algebra.ssralg]
GRing.zmodClosedP [lemma, in mathcomp.algebra.ssralg]
GRing.ZmodExports [module, in mathcomp.algebra.ssralg]
GRing.ZmodExports.ZmodMixin [abbreviation, in mathcomp.algebra.ssralg]
[ zmodType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
[ zmodType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
GRing.ZmodulePred [section, in mathcomp.algebra.ssralg]
GRing.ZmodulePred.Opp [section, in mathcomp.algebra.ssralg]
GRing.ZmodulePred.Opp.S [variable, in mathcomp.algebra.ssralg]
GRing.ZmodulePred.Sub [section, in mathcomp.algebra.ssralg]
GRing.ZmodulePred.Sub.S [variable, in mathcomp.algebra.ssralg]
GRing.ZmodulePred.V [variable, in mathcomp.algebra.ssralg]
GRing.ZmoduleTheory [section, in mathcomp.algebra.ssralg]
GRing.ZmoduleTheory.ClosedPredicates [section, in mathcomp.algebra.ssralg]
GRing.ZmoduleTheory.ClosedPredicates.S [variable, in mathcomp.algebra.ssralg]
GRing.ZmoduleTheory.V [variable, in mathcomp.algebra.ssralg]
GRing.zmod_closedD [lemma, in mathcomp.algebra.ssralg]
GRing.zmod_closedN [lemma, in mathcomp.algebra.ssralg]
GRing.zmod_closed [definition, in mathcomp.algebra.ssralg]
_ \* _ (function_scope) [notation, in mathcomp.algebra.ssralg]
_ \o* _ (function_scope) [notation, in mathcomp.algebra.ssralg]
_ \*o _ (function_scope) [notation, in mathcomp.algebra.ssralg]
_ \*: _ (function_scope) [notation, in mathcomp.algebra.ssralg]
\- _ (function_scope) [notation, in mathcomp.algebra.ssralg]
_ \- _ (function_scope) [notation, in mathcomp.algebra.ssralg]
_ \+ _ (function_scope) [notation, in mathcomp.algebra.ssralg]
\0 (function_scope) [notation, in mathcomp.algebra.ssralg]
*:%R (function_scope) [notation, in mathcomp.algebra.ssralg]
*%R (function_scope) [notation, in mathcomp.algebra.ssralg]
+%R (function_scope) [notation, in mathcomp.algebra.ssralg]
_ %:A (ring_scope) [notation, in mathcomp.algebra.ssralg]
_ *: _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
- 1 (ring_scope) [notation, in mathcomp.algebra.ssralg]
_ ^+ _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
_ * _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
_ %:R (ring_scope) [notation, in mathcomp.algebra.ssralg]
1 (ring_scope) [notation, in mathcomp.algebra.ssralg]
_ *- _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
_ - _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
- _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
-%R (ring_scope) [notation, in mathcomp.algebra.ssralg]
_ `_ _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
_ *+ _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
_ + _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
0 (ring_scope) [notation, in mathcomp.algebra.ssralg]
'forall 'X_ _ , _ (term_scope) [notation, in mathcomp.algebra.ssralg]
'exists 'X_ _ , _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ != _ (term_scope) [notation, in mathcomp.algebra.ssralg]
~ _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ ==> _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ \/ _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ /\ _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ == _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ ^+ _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ / _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ ^-1 (term_scope) [notation, in mathcomp.algebra.ssralg]
_ *+ _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ * _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ - _ (term_scope) [notation, in mathcomp.algebra.ssralg]
- _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ + _ (term_scope) [notation, in mathcomp.algebra.ssralg]
1 (term_scope) [notation, in mathcomp.algebra.ssralg]
0 (term_scope) [notation, in mathcomp.algebra.ssralg]
_ %:T (term_scope) [notation, in mathcomp.algebra.ssralg]
_ %:R (term_scope) [notation, in mathcomp.algebra.ssralg]
'X_ _ (term_scope) [notation, in mathcomp.algebra.ssralg]
_ ^o (type_scope) [notation, in mathcomp.algebra.ssralg]
_ ^c (type_scope) [notation, in mathcomp.algebra.ssralg]
_ ^- _ [notation, in mathcomp.algebra.ssralg]
_ / _ [notation, in mathcomp.algebra.ssralg]
_ ^-1 [notation, in mathcomp.algebra.ssralg]
\prod_ ( _ <= _ < _ ) _ [notation, in mathcomp.algebra.ssralg]
\prod_ ( _ in _ ) _ [notation, in mathcomp.algebra.ssralg]
\prod_ ( _ | _ ) _ [notation, in mathcomp.algebra.ssralg]
\prod_ ( _ <- _ | _ ) _ [notation, in mathcomp.algebra.ssralg]
\sum_ ( _ in _ ) _ [notation, in mathcomp.algebra.ssralg]
\sum_ ( _ < _ ) _ [notation, in mathcomp.algebra.ssralg]
\sum_ ( _ <= _ < _ ) _ [notation, in mathcomp.algebra.ssralg]
\sum_ ( _ <- _ | _ ) _ [notation, in mathcomp.algebra.ssralg]
group [definition, in mathcomp.fingroup.fingroup]
groupAction [record, in mathcomp.fingroup.action]
GroupAction [section, in mathcomp.fingroup.action]
GroupActionDefs [section, in mathcomp.fingroup.action]
GroupActionDefs.aT [variable, in mathcomp.fingroup.action]
GroupActionDefs.D [variable, in mathcomp.fingroup.action]
GroupActionDefs.R [variable, in mathcomp.fingroup.action]
GroupActionDefs.rT [variable, in mathcomp.fingroup.action]
GroupActionTheory [section, in mathcomp.fingroup.action]
GroupActionTheory.ActBy [section, in mathcomp.fingroup.action]
GroupActionTheory.ActBy.A [variable, in mathcomp.fingroup.action]
GroupActionTheory.ActBy.G [variable, in mathcomp.fingroup.action]
GroupActionTheory.ActBy.nGAg [variable, in mathcomp.fingroup.action]
GroupActionTheory.aT [variable, in mathcomp.fingroup.action]
GroupActionTheory.CompAct [section, in mathcomp.fingroup.action]
GroupActionTheory.CompAct.f [variable, in mathcomp.fingroup.action]
GroupActionTheory.CompAct.G [variable, in mathcomp.fingroup.action]
GroupActionTheory.CompAct.gT [variable, in mathcomp.fingroup.action]
GroupActionTheory.D [variable, in mathcomp.fingroup.action]
GroupActionTheory.Mod [section, in mathcomp.fingroup.action]
GroupActionTheory.Mod.H [variable, in mathcomp.fingroup.action]
GroupActionTheory.Quotient [section, in mathcomp.fingroup.action]
GroupActionTheory.Quotient.H [variable, in mathcomp.fingroup.action]
GroupActionTheory.R [variable, in mathcomp.fingroup.action]
GroupActionTheory.Restrict [section, in mathcomp.fingroup.action]
GroupActionTheory.Restrict.A [variable, in mathcomp.fingroup.action]
GroupActionTheory.Restrict.sAD [variable, in mathcomp.fingroup.action]
GroupActionTheory.rT [variable, in mathcomp.fingroup.action]
GroupActionTheory.to [variable, in mathcomp.fingroup.action]
GroupAction.aT [variable, in mathcomp.fingroup.action]
GroupAction.D [variable, in mathcomp.fingroup.action]
GroupAction.R [variable, in mathcomp.fingroup.action]
GroupAction.rT [variable, in mathcomp.fingroup.action]
groupC [lemma, in mathcomp.character.character]
GroupDefs [section, in mathcomp.solvable.gseries]
GroupDefs.gT [variable, in mathcomp.solvable.gseries]
groupD1_inj [lemma, in mathcomp.fingroup.fingroup]
GroupIdentities [section, in mathcomp.fingroup.fingroup]
GroupIdentities.T [variable, in mathcomp.fingroup.fingroup]
GroupInter [section, in mathcomp.fingroup.fingroup]
GroupInter.gT [variable, in mathcomp.fingroup.fingroup]
GroupInter.Nary [section, in mathcomp.fingroup.fingroup]
GroupInter.Nary.F [variable, in mathcomp.fingroup.fingroup]
GroupInter.Nary.I [variable, in mathcomp.fingroup.fingroup]
GroupInter.Nary.P [variable, in mathcomp.fingroup.fingroup]
groupJ [lemma, in mathcomp.fingroup.fingroup]
groupJr [lemma, in mathcomp.fingroup.fingroup]
groupM [lemma, in mathcomp.fingroup.fingroup]
groupMl [lemma, in mathcomp.fingroup.fingroup]
groupMr [lemma, in mathcomp.fingroup.fingroup]
groupP [lemma, in mathcomp.fingroup.fingroup]
GroupProp [section, in mathcomp.fingroup.fingroup]
GroupProp.gT [variable, in mathcomp.fingroup.fingroup]
GroupProp.OneGroup [section, in mathcomp.fingroup.fingroup]
GroupProp.OneGroup.G [variable, in mathcomp.fingroup.fingroup]
groupR [lemma, in mathcomp.fingroup.fingroup]
Groups [section, in mathcomp.algebra.zmodp]
GroupScope [module, in mathcomp.fingroup.fingroup]
GroupSet [module, in mathcomp.fingroup.fingroup]
GroupSetBaseGroup [module, in mathcomp.fingroup.fingroup]
GroupSetBaseGroupSig [module, in mathcomp.fingroup.fingroup]
GroupSetBaseGroupSig.sort [definition, in mathcomp.fingroup.fingroup]
GroupSetMulDef [section, in mathcomp.fingroup.fingroup]
GroupSetMulDef.gT [variable, in mathcomp.fingroup.fingroup]
GroupSetMulProp [section, in mathcomp.fingroup.fingroup]
GroupSetMulProp.gT [variable, in mathcomp.fingroup.fingroup]
GroupSet.sort [definition, in mathcomp.fingroup.fingroup]
Groups.p [variable, in mathcomp.algebra.zmodp]
groupT [abbreviation, in mathcomp.fingroup.fingroup]
groupT [abbreviation, in mathcomp.solvable.gseries]
groupV [lemma, in mathcomp.fingroup.fingroup]
groupVl [lemma, in mathcomp.fingroup.fingroup]
groupVr [lemma, in mathcomp.fingroup.fingroup]
groupX [lemma, in mathcomp.fingroup.fingroup]
group_num_field_exists [lemma, in mathcomp.character.integral_char]
group_set_inertia [lemma, in mathcomp.character.inertia]
group_set_gacent [lemma, in mathcomp.fingroup.action]
group_set_astabs [lemma, in mathcomp.fingroup.action]
group_set_astab [lemma, in mathcomp.fingroup.action]
group_set_normaliser [lemma, in mathcomp.fingroup.fingroup]
group_set_generated [lemma, in mathcomp.fingroup.fingroup]
group_set_bigcap [lemma, in mathcomp.fingroup.fingroup]
group_setI [lemma, in mathcomp.fingroup.fingroup]
group_modr [lemma, in mathcomp.fingroup.fingroup]
group_modl [lemma, in mathcomp.fingroup.fingroup]
group_set_conjG [lemma, in mathcomp.fingroup.fingroup]
group_setJ [lemma, in mathcomp.fingroup.fingroup]
group_prod [lemma, in mathcomp.fingroup.fingroup]
group_setT [lemma, in mathcomp.fingroup.fingroup]
group_set_one [lemma, in mathcomp.fingroup.fingroup]
group_inj [lemma, in mathcomp.fingroup.fingroup]
group_of [definition, in mathcomp.fingroup.fingroup]
group_type [record, in mathcomp.fingroup.fingroup]
group_setP [lemma, in mathcomp.fingroup.fingroup]
group_set [definition, in mathcomp.fingroup.fingroup]
group_closure_closed_field [lemma, in mathcomp.character.mxrepresentation]
group_closure_field_exists [lemma, in mathcomp.character.mxrepresentation]
group_splitting_field_exists [lemma, in mathcomp.character.mxrepresentation]
group_closure_field [definition, in mathcomp.character.mxrepresentation]
group_splitting_field [definition, in mathcomp.character.mxrepresentation]
group_ring [definition, in mathcomp.character.mxrepresentation]
group_setX [lemma, in mathcomp.fingroup.gproduct]
group_not0 [lemma, in mathcomp.fingroup.gproduct]
group_Ldiv [lemma, in mathcomp.solvable.abelian]
group_rel_of [definition, in mathcomp.solvable.gseries]
group_set_diso3 [lemma, in mathcomp.solvable.burnside_app]
group_set_iso3 [lemma, in mathcomp.solvable.burnside_app]
group_set_rotations [lemma, in mathcomp.solvable.burnside_app]
group_set_iso [lemma, in mathcomp.solvable.burnside_app]
group_set_iso2 [lemma, in mathcomp.solvable.burnside_app]
group_set_rot [lemma, in mathcomp.solvable.burnside_app]
group0 [lemma, in mathcomp.fingroup.gproduct]
group1 [lemma, in mathcomp.fingroup.fingroup]
group1_contra [lemma, in mathcomp.fingroup.fingroup]
Grp_quaternion [lemma, in mathcomp.solvable.extremal]
Grp_semidihedral [lemma, in mathcomp.solvable.extremal]
Grp_2dihedral [lemma, in mathcomp.solvable.extremal]
Grp_dihedral [lemma, in mathcomp.solvable.extremal]
Grp_ext_dihedral [lemma, in mathcomp.solvable.extremal]
Grp_modular_group [lemma, in mathcomp.solvable.extremal]
Grp_pX1p2 [lemma, in mathcomp.solvable.extraspecial]
Grp'_dihedral [lemma, in mathcomp.solvable.extremal]
GSection [constructor, in mathcomp.solvable.jordanholder]
gseries [library]
gset_mx [definition, in mathcomp.character.mxrepresentation]
gsimp [definition, in mathcomp.fingroup.fingroup]
gsort [abbreviation, in mathcomp.fingroup.fingroup]
gT [abbreviation, in mathcomp.fingroup.action]
gTg [abbreviation, in mathcomp.solvable.jordanholder]
gtn [definition, in mathcomp.ssreflect.ssrnat]
gtnNdvd [lemma, in mathcomp.ssreflect.div]
GtnNotLeq [constructor, in mathcomp.ssreflect.ssrnat]
gtn_uphalf_double [lemma, in mathcomp.ssreflect.ssrnat]
gtn_half_double [lemma, in mathcomp.ssreflect.ssrnat]
gtn_min [lemma, in mathcomp.ssreflect.ssrnat]
gtn_max [lemma, in mathcomp.ssreflect.ssrnat]
gtn_eqF [lemma, in mathcomp.ssreflect.ssrnat]
gtr0_sgz [lemma, in mathcomp.algebra.ssrint]
gtype [abbreviation, in mathcomp.solvable.extraspecial]
gtz0_abs [lemma, in mathcomp.algebra.ssrint]
gtz0_ge1 [lemma, in mathcomp.algebra.ssrint]
gt_pinfty [lemma, in mathcomp.algebra.interval]
gt_rat0 [lemma, in mathcomp.algebra.rat]
gt_size_poly_neq0 [lemma, in mathcomp.algebra.poly]
gt0CG [lemma, in mathcomp.character.classfun]
gt0CiG [lemma, in mathcomp.character.classfun]
gT:1 [binder, in mathcomp.character.integral_char]
gT:1 [binder, in mathcomp.solvable.finmodule]
gT:1 [binder, in mathcomp.solvable.jordanholder]
gT:1 [binder, in mathcomp.solvable.burnside_app]
gT:1 [binder, in mathcomp.solvable.hall]
gT:1 [binder, in mathcomp.solvable.gfunctor]
gT:10 [binder, in mathcomp.solvable.jordanholder]
gT:101 [binder, in mathcomp.solvable.gfunctor]
gT:1014 [binder, in mathcomp.character.character]
gT:102 [binder, in mathcomp.solvable.extremal]
gT:102 [binder, in mathcomp.solvable.maximal]
gT:1031 [binder, in mathcomp.character.character]
gT:1035 [binder, in mathcomp.character.character]
gT:106 [binder, in mathcomp.solvable.gfunctor]
gT:107 [binder, in mathcomp.solvable.hall]
gT:108 [binder, in mathcomp.solvable.extremal]
gT:11 [binder, in mathcomp.solvable.gfunctor]
gT:111 [binder, in mathcomp.solvable.gfunctor]
gT:117 [binder, in mathcomp.solvable.gfunctor]
gT:12 [binder, in mathcomp.solvable.jordanholder]
gT:122 [binder, in mathcomp.character.integral_char]
gT:122 [binder, in mathcomp.solvable.gfunctor]
gT:123 [binder, in mathcomp.character.mxabelem]
gT:125 [binder, in mathcomp.character.integral_char]
gT:128 [binder, in mathcomp.solvable.gfunctor]
gT:129 [binder, in mathcomp.character.integral_char]
gT:130 [binder, in mathcomp.solvable.extremal]
gT:131 [binder, in mathcomp.solvable.gfunctor]
gT:133 [binder, in mathcomp.solvable.extremal]
gT:137 [binder, in mathcomp.solvable.extremal]
gT:143 [binder, in mathcomp.character.integral_char]
gT:143 [binder, in mathcomp.solvable.gfunctor]
gT:1439 [binder, in mathcomp.character.mxrepresentation]
gT:144 [binder, in mathcomp.solvable.gfunctor]
gT:145 [binder, in mathcomp.solvable.gseries]
gT:148 [binder, in mathcomp.solvable.gseries]
gT:149 [binder, in mathcomp.solvable.sylow]
gT:15 [binder, in mathcomp.solvable.gfunctor]
gT:151 [binder, in mathcomp.solvable.gseries]
gT:152 [binder, in mathcomp.solvable.sylow]
gT:153 [binder, in mathcomp.solvable.finmodule]
gT:155 [binder, in mathcomp.solvable.gseries]
gT:159 [binder, in mathcomp.solvable.nilpotent]
gT:16 [binder, in mathcomp.solvable.hall]
gT:161 [binder, in mathcomp.solvable.nilpotent]
gT:163 [binder, in mathcomp.solvable.frobenius]
gT:163 [binder, in mathcomp.solvable.nilpotent]
gT:1634 [binder, in mathcomp.character.mxrepresentation]
gT:1644 [binder, in mathcomp.character.mxrepresentation]
gT:1652 [binder, in mathcomp.character.mxrepresentation]
gT:174 [binder, in mathcomp.character.classfun]
gT:177 [binder, in mathcomp.character.integral_char]
gT:1829 [binder, in mathcomp.algebra.ssrnum]
gT:186 [binder, in mathcomp.solvable.frobenius]
gT:190 [binder, in mathcomp.character.integral_char]
gT:198 [binder, in mathcomp.character.integral_char]
gT:199 [binder, in mathcomp.solvable.extremal]
gT:2 [binder, in mathcomp.solvable.commutator]
gT:20 [binder, in mathcomp.solvable.gfunctor]
gT:220 [binder, in mathcomp.fingroup.fingroup]
gT:221 [binder, in mathcomp.fingroup.fingroup]
gT:222 [binder, in mathcomp.fingroup.fingroup]
gT:226 [binder, in mathcomp.character.integral_char]
gT:23 [binder, in mathcomp.solvable.hall]
gT:23 [binder, in mathcomp.solvable.gfunctor]
gT:233 [binder, in mathcomp.fingroup.quotient]
gT:24 [binder, in mathcomp.fingroup.presentation]
gT:241 [binder, in mathcomp.character.character]
gT:249 [binder, in mathcomp.character.character]
gT:29 [binder, in mathcomp.solvable.gfunctor]
gT:3 [binder, in mathcomp.solvable.gfunctor]
gT:3 [binder, in mathcomp.fingroup.presentation]
gT:308 [binder, in mathcomp.character.vcharacter]
gT:31 [binder, in mathcomp.solvable.gfunctor]
gT:32 [binder, in mathcomp.solvable.extremal]
gT:33 [binder, in mathcomp.fingroup.presentation]
gT:36 [binder, in mathcomp.fingroup.presentation]
gT:372 [binder, in mathcomp.solvable.extremal]
gT:38 [binder, in mathcomp.fingroup.presentation]
gT:393 [binder, in mathcomp.solvable.extremal]
gT:4 [binder, in mathcomp.solvable.jordanholder]
gT:4 [binder, in mathcomp.solvable.hall]
gT:40 [binder, in mathcomp.solvable.extraspecial]
gT:409 [binder, in mathcomp.solvable.extremal]
gT:420 [binder, in mathcomp.solvable.extremal]
gT:428 [binder, in mathcomp.solvable.extremal]
gT:431 [binder, in mathcomp.solvable.extremal]
gT:434 [binder, in mathcomp.solvable.extremal]
gT:439 [binder, in mathcomp.fingroup.morphism]
gT:447 [binder, in mathcomp.solvable.pgroup]
gT:453 [binder, in mathcomp.fingroup.morphism]
gT:454 [binder, in mathcomp.solvable.pgroup]
gT:458 [binder, in mathcomp.solvable.pgroup]
gT:459 [binder, in mathcomp.fingroup.morphism]
gT:461 [binder, in mathcomp.solvable.pgroup]
gT:465 [binder, in mathcomp.solvable.pgroup]
gT:472 [binder, in mathcomp.solvable.pgroup]
gT:477 [binder, in mathcomp.solvable.pgroup]
gT:481 [binder, in mathcomp.solvable.pgroup]
gT:491 [binder, in mathcomp.solvable.pgroup]
gT:494 [binder, in mathcomp.solvable.pgroup]
gT:497 [binder, in mathcomp.solvable.pgroup]
gT:5 [binder, in mathcomp.solvable.gfunctor]
gT:501 [binder, in mathcomp.solvable.pgroup]
gT:505 [binder, in mathcomp.solvable.pgroup]
gT:509 [binder, in mathcomp.solvable.pgroup]
gT:51 [binder, in mathcomp.fingroup.presentation]
gT:513 [binder, in mathcomp.solvable.pgroup]
gT:517 [binder, in mathcomp.solvable.pgroup]
gT:52 [binder, in mathcomp.solvable.extraspecial]
gT:521 [binder, in mathcomp.solvable.pgroup]
gT:525 [binder, in mathcomp.solvable.pgroup]
gT:529 [binder, in mathcomp.solvable.pgroup]
gT:533 [binder, in mathcomp.solvable.pgroup]
gT:537 [binder, in mathcomp.solvable.pgroup]
gT:54 [binder, in mathcomp.fingroup.presentation]
gT:541 [binder, in mathcomp.solvable.pgroup]
gT:545 [binder, in mathcomp.solvable.pgroup]
gT:549 [binder, in mathcomp.solvable.pgroup]
gT:552 [binder, in mathcomp.solvable.pgroup]
gT:557 [binder, in mathcomp.solvable.pgroup]
gT:561 [binder, in mathcomp.solvable.pgroup]
gT:563 [binder, in mathcomp.fingroup.fingroup]
gT:565 [binder, in mathcomp.solvable.pgroup]
gT:568 [binder, in mathcomp.fingroup.fingroup]
gT:576 [binder, in mathcomp.fingroup.fingroup]
gT:579 [binder, in mathcomp.fingroup.fingroup]
gT:582 [binder, in mathcomp.fingroup.fingroup]
gT:584 [binder, in mathcomp.fingroup.fingroup]
gT:62 [binder, in mathcomp.fingroup.presentation]
gT:642 [binder, in mathcomp.solvable.abelian]
gT:646 [binder, in mathcomp.solvable.abelian]
gT:65 [binder, in mathcomp.fingroup.presentation]
gT:66 [binder, in mathcomp.solvable.gfunctor]
gT:68 [binder, in mathcomp.solvable.gfunctor]
gT:7 [binder, in mathcomp.solvable.finmodule]
gT:7 [binder, in mathcomp.solvable.jordanholder]
gT:7 [binder, in mathcomp.solvable.gfunctor]
gT:71 [binder, in mathcomp.fingroup.presentation]
gT:74 [binder, in mathcomp.solvable.extraspecial]
gT:749 [binder, in mathcomp.character.character]
gT:75 [binder, in mathcomp.solvable.gfunctor]
gT:776 [binder, in mathcomp.character.classfun]
gT:78 [binder, in mathcomp.solvable.gfunctor]
gT:79 [binder, in mathcomp.character.integral_char]
gT:796 [binder, in mathcomp.character.mxrepresentation]
gT:80 [binder, in mathcomp.solvable.gfunctor]
gT:80 [binder, in mathcomp.solvable.extraspecial]
gT:800 [binder, in mathcomp.character.mxrepresentation]
gT:802 [binder, in mathcomp.character.mxrepresentation]
gT:805 [binder, in mathcomp.character.mxrepresentation]
gT:82 [binder, in mathcomp.solvable.extraspecial]
gT:83 [binder, in mathcomp.solvable.gfunctor]
gT:84 [binder, in mathcomp.solvable.gfunctor]
gT:85 [binder, in mathcomp.fingroup.presentation]
gT:86 [binder, in mathcomp.solvable.gfunctor]
gT:874 [binder, in mathcomp.fingroup.action]
gT:88 [binder, in mathcomp.solvable.gfunctor]
gT:90 [binder, in mathcomp.solvable.gfunctor]
gT:90 [binder, in mathcomp.fingroup.presentation]
gT:92 [binder, in mathcomp.solvable.gfunctor]
gT:95 [binder, in mathcomp.solvable.gfunctor]
gT:95 [binder, in mathcomp.fingroup.presentation]
gT:98 [binder, in mathcomp.solvable.gfunctor]
gT:986 [binder, in mathcomp.character.character]
gT:99 [binder, in mathcomp.solvable.maximal]
gval [projection, in mathcomp.fingroup.fingroup]
gX [definition, in mathcomp.field.qfpoly]
gX_all [lemma, in mathcomp.field.qfpoly]
gX_order [lemma, in mathcomp.field.qfpoly]
Gx:1002 [binder, in mathcomp.character.mxrepresentation]
Gx:197 [binder, in mathcomp.fingroup.quotient]
Gx:200 [binder, in mathcomp.fingroup.quotient]
gz:140 [binder, in mathcomp.solvable.center]
gz:146 [binder, in mathcomp.solvable.center]
G_ [abbreviation, in mathcomp.solvable.center]
G' [abbreviation, in mathcomp.solvable.hall]
g':170 [binder, in mathcomp.algebra.matrix]
g':176 [binder, in mathcomp.algebra.matrix]
g':1955 [binder, in mathcomp.algebra.matrix]
g':1958 [binder, in mathcomp.algebra.matrix]
g':2291 [binder, in mathcomp.algebra.matrix]
g':360 [binder, in mathcomp.algebra.matrix]
g':374 [binder, in mathcomp.algebra.matrix]
G0:506 [binder, in mathcomp.character.inertia]
G0:507 [binder, in mathcomp.character.inertia]
G1 [abbreviation, in mathcomp.character.classfun]
g1:103 [binder, in mathcomp.ssreflect.finfun]
G1:120 [binder, in mathcomp.fingroup.quotient]
g1:148 [binder, in mathcomp.character.integral_char]
G1:152 [binder, in mathcomp.solvable.frobenius]
G1:18 [binder, in mathcomp.solvable.jordanholder]
G1:187 [binder, in mathcomp.fingroup.gproduct]
G1:193 [binder, in mathcomp.fingroup.gproduct]
G1:5 [binder, in mathcomp.solvable.jordanholder]
g1:51 [binder, in mathcomp.ssreflect.finfun]
g1:743 [binder, in mathcomp.algebra.vector]
g2:104 [binder, in mathcomp.ssreflect.finfun]
G2:121 [binder, in mathcomp.fingroup.quotient]
g2:149 [binder, in mathcomp.character.integral_char]
G2:19 [binder, in mathcomp.solvable.jordanholder]
g2:52 [binder, in mathcomp.ssreflect.finfun]
G2:6 [binder, in mathcomp.solvable.jordanholder]
g2:744 [binder, in mathcomp.algebra.vector]
G:1 [binder, in mathcomp.fingroup.fingroup]
G:10 [binder, in mathcomp.solvable.commutator]
G:10 [binder, in mathcomp.character.mxrepresentation]
G:10 [binder, in mathcomp.solvable.gseries]
G:10 [binder, in mathcomp.solvable.center]
G:10 [binder, in mathcomp.solvable.nilpotent]
G:100 [binder, in mathcomp.solvable.commutator]
G:100 [binder, in mathcomp.solvable.abelian]
G:100 [binder, in mathcomp.solvable.gfunctor]
G:100 [binder, in mathcomp.solvable.maximal]
G:1001 [binder, in mathcomp.fingroup.fingroup]
G:101 [binder, in mathcomp.solvable.sylow]
G:101 [binder, in mathcomp.solvable.pgroup]
g:101 [binder, in mathcomp.ssreflect.order]
G:101 [binder, in mathcomp.solvable.frobenius]
G:101 [binder, in mathcomp.solvable.hall]
G:1015 [binder, in mathcomp.character.character]
G:102 [binder, in mathcomp.fingroup.quotient]
G:102 [binder, in mathcomp.fingroup.automorphism]
G:1021 [binder, in mathcomp.character.character]
G:1026 [binder, in mathcomp.character.character]
G:103 [binder, in mathcomp.solvable.commutator]
G:103 [binder, in mathcomp.solvable.abelian]
g:103 [binder, in mathcomp.ssreflect.ssrbool]
G:103 [binder, in mathcomp.solvable.gfunctor]
G:103 [binder, in mathcomp.solvable.maximal]
G:1032 [binder, in mathcomp.character.character]
G:1036 [binder, in mathcomp.character.character]
G:1037 [binder, in mathcomp.fingroup.fingroup]
g:1038 [binder, in mathcomp.character.character]
g:1039 [binder, in mathcomp.character.character]
g:104 [binder, in mathcomp.character.integral_char]
G:104 [binder, in mathcomp.fingroup.quotient]
G:104 [binder, in mathcomp.solvable.pgroup]
G:104 [binder, in mathcomp.solvable.hall]
G:1040 [binder, in mathcomp.fingroup.fingroup]
g:1040 [binder, in mathcomp.character.character]
g:1042 [binder, in mathcomp.algebra.matrix]
G:1051 [binder, in mathcomp.fingroup.fingroup]
G:106 [binder, in mathcomp.solvable.commutator]
G:106 [binder, in mathcomp.fingroup.automorphism]
G:106 [binder, in mathcomp.solvable.nilpotent]
g:107 [binder, in mathcomp.algebra.matrix]
G:107 [binder, in mathcomp.fingroup.automorphism]
G:107 [binder, in mathcomp.solvable.cyclic]
G:108 [binder, in mathcomp.solvable.sylow]
G:108 [binder, in mathcomp.solvable.pgroup]
G:108 [binder, in mathcomp.fingroup.gproduct]
G:108 [binder, in mathcomp.solvable.gfunctor]
G:109 [binder, in mathcomp.solvable.commutator]
G:109 [binder, in mathcomp.solvable.jordanholder]
G:109 [binder, in mathcomp.fingroup.automorphism]
G:109 [binder, in mathcomp.solvable.extremal]
G:109 [binder, in mathcomp.solvable.cyclic]
G:109 [binder, in mathcomp.solvable.hall]
G:1095 [binder, in mathcomp.fingroup.fingroup]
G:1097 [binder, in mathcomp.fingroup.fingroup]
G:11 [binder, in mathcomp.solvable.frobenius]
G:11 [binder, in mathcomp.solvable.nilpotent]
G:1100 [binder, in mathcomp.fingroup.fingroup]
G:1102 [binder, in mathcomp.fingroup.fingroup]
G:1104 [binder, in mathcomp.fingroup.fingroup]
G:1106 [binder, in mathcomp.fingroup.fingroup]
G:111 [binder, in mathcomp.solvable.jordanholder]
G:111 [binder, in mathcomp.solvable.cyclic]
g:111 [binder, in mathcomp.character.character]
G:1116 [binder, in mathcomp.fingroup.fingroup]
G:1118 [binder, in mathcomp.fingroup.fingroup]
G:1119 [binder, in mathcomp.fingroup.fingroup]
G:112 [binder, in mathcomp.fingroup.quotient]
G:112 [binder, in mathcomp.fingroup.automorphism]
G:112 [binder, in mathcomp.solvable.frobenius]
G:1123 [binder, in mathcomp.fingroup.fingroup]
G:1126 [binder, in mathcomp.fingroup.fingroup]
G:113 [binder, in mathcomp.solvable.pgroup]
G:113 [binder, in mathcomp.solvable.abelian]
G:113 [binder, in mathcomp.solvable.gfunctor]
G:1135 [binder, in mathcomp.fingroup.fingroup]
G:1138 [binder, in mathcomp.fingroup.fingroup]
G:114 [binder, in mathcomp.solvable.sylow]
G:114 [binder, in mathcomp.solvable.cyclic]
g:115 [binder, in mathcomp.field.galois]
G:115 [binder, in mathcomp.solvable.frobenius]
G:115 [binder, in mathcomp.fingroup.gproduct]
G:116 [binder, in mathcomp.fingroup.automorphism]
G:117 [binder, in mathcomp.fingroup.quotient]
G:117 [binder, in mathcomp.solvable.pgroup]
G:117 [binder, in mathcomp.solvable.cyclic]
G:1170 [binder, in mathcomp.fingroup.fingroup]
G:1173 [binder, in mathcomp.fingroup.fingroup]
G:1174 [binder, in mathcomp.fingroup.fingroup]
G:1175 [binder, in mathcomp.fingroup.fingroup]
G:1176 [binder, in mathcomp.fingroup.fingroup]
G:118 [binder, in mathcomp.fingroup.quotient]
G:118 [binder, in mathcomp.solvable.commutator]
G:118 [binder, in mathcomp.solvable.sylow]
G:118 [binder, in mathcomp.solvable.frobenius]
G:118 [binder, in mathcomp.fingroup.gproduct]
G:118 [binder, in mathcomp.solvable.maximal]
G:118 [binder, in mathcomp.solvable.nilpotent]
G:1181 [binder, in mathcomp.fingroup.fingroup]
G:1184 [binder, in mathcomp.fingroup.fingroup]
G:1187 [binder, in mathcomp.fingroup.fingroup]
G:1187 [binder, in mathcomp.algebra.ssrnum]
G:1189 [binder, in mathcomp.fingroup.fingroup]
G:119 [binder, in mathcomp.fingroup.quotient]
G:119 [binder, in mathcomp.fingroup.automorphism]
G:119 [binder, in mathcomp.solvable.gfunctor]
G:1191 [binder, in mathcomp.fingroup.fingroup]
G:1194 [binder, in mathcomp.fingroup.fingroup]
G:1196 [binder, in mathcomp.fingroup.fingroup]
G:1199 [binder, in mathcomp.fingroup.fingroup]
G:12 [binder, in mathcomp.solvable.commutator]
G:12 [binder, in mathcomp.solvable.center]
G:120 [binder, in mathcomp.solvable.jordanholder]
G:120 [binder, in mathcomp.solvable.cyclic]
G:120 [binder, in mathcomp.solvable.maximal]
G:1202 [binder, in mathcomp.fingroup.fingroup]
G:1204 [binder, in mathcomp.fingroup.fingroup]
G:1206 [binder, in mathcomp.fingroup.fingroup]
G:1208 [binder, in mathcomp.fingroup.fingroup]
G:121 [binder, in mathcomp.solvable.pgroup]
G:121 [binder, in mathcomp.fingroup.gproduct]
G:1211 [binder, in mathcomp.fingroup.fingroup]
G:1214 [binder, in mathcomp.fingroup.fingroup]
G:1215 [binder, in mathcomp.fingroup.fingroup]
G:1218 [binder, in mathcomp.fingroup.fingroup]
G:122 [binder, in mathcomp.fingroup.automorphism]
G:122 [binder, in mathcomp.solvable.frobenius]
G:122 [binder, in mathcomp.solvable.abelian]
g:1220 [binder, in mathcomp.algebra.mxalgebra]
g:1221 [binder, in mathcomp.algebra.mxalgebra]
G:123 [binder, in mathcomp.character.integral_char]
G:124 [binder, in mathcomp.fingroup.automorphism]
G:124 [binder, in mathcomp.solvable.pgroup]
G:124 [binder, in mathcomp.fingroup.gproduct]
G:124 [binder, in mathcomp.solvable.abelian]
G:124 [binder, in mathcomp.solvable.gfunctor]
G:1243 [binder, in mathcomp.fingroup.fingroup]
G:1245 [binder, in mathcomp.fingroup.fingroup]
G:125 [binder, in mathcomp.solvable.commutator]
G:125 [binder, in mathcomp.fingroup.automorphism]
G:125 [binder, in mathcomp.solvable.frobenius]
G:125 [binder, in mathcomp.fingroup.morphism]
G:125 [binder, in mathcomp.solvable.cyclic]
G:125 [binder, in mathcomp.solvable.nilpotent]
G:126 [binder, in mathcomp.character.integral_char]
G:126 [binder, in mathcomp.solvable.sylow]
G:126 [binder, in mathcomp.solvable.frobenius]
g:127 [binder, in mathcomp.ssreflect.finfun]
G:127 [binder, in mathcomp.solvable.sylow]
G:127 [binder, in mathcomp.solvable.abelian]
G:1275 [binder, in mathcomp.fingroup.fingroup]
G:1278 [binder, in mathcomp.fingroup.fingroup]
G:128 [binder, in mathcomp.fingroup.automorphism]
G:128 [binder, in mathcomp.solvable.sylow]
G:128 [binder, in mathcomp.solvable.pgroup]
G:128 [binder, in mathcomp.solvable.frobenius]
G:128 [binder, in mathcomp.fingroup.gproduct]
G:128 [binder, in mathcomp.fingroup.morphism]
G:128 [binder, in mathcomp.solvable.cyclic]
G:128 [binder, in mathcomp.solvable.nilpotent]
G:1289 [binder, in mathcomp.fingroup.fingroup]
g:129 [binder, in mathcomp.field.galois]
G:129 [binder, in mathcomp.solvable.gfunctor]
G:129 [binder, in mathcomp.solvable.nilpotent]
G:13 [binder, in mathcomp.solvable.frobenius]
G:13 [binder, in mathcomp.solvable.gfunctor]
G:13 [binder, in mathcomp.solvable.maximal]
G:13 [binder, in mathcomp.solvable.nilpotent]
G:130 [binder, in mathcomp.character.integral_char]
G:130 [binder, in mathcomp.solvable.sylow]
G:130 [binder, in mathcomp.solvable.frobenius]
G:130 [binder, in mathcomp.solvable.cyclic]
G:1303 [binder, in mathcomp.fingroup.fingroup]
G:1304 [binder, in mathcomp.fingroup.fingroup]
g:1306 [binder, in mathcomp.ssreflect.seq]
G:1306 [binder, in mathcomp.fingroup.fingroup]
G:1307 [binder, in mathcomp.fingroup.fingroup]
g:1308 [binder, in mathcomp.ssreflect.seq]
G:131 [binder, in mathcomp.fingroup.automorphism]
G:131 [binder, in mathcomp.fingroup.gproduct]
G:131 [binder, in mathcomp.solvable.cyclic]
G:131 [binder, in mathcomp.solvable.nilpotent]
g:1311 [binder, in mathcomp.ssreflect.seq]
g:1314 [binder, in mathcomp.ssreflect.seq]
g:1319 [binder, in mathcomp.ssreflect.seq]
G:132 [binder, in mathcomp.fingroup.morphism]
G:132 [binder, in mathcomp.solvable.gfunctor]
G:132 [binder, in mathcomp.solvable.nilpotent]
G:1321 [binder, in mathcomp.fingroup.fingroup]
G:1322 [binder, in mathcomp.fingroup.fingroup]
G:1323 [binder, in mathcomp.fingroup.fingroup]
G:1324 [binder, in mathcomp.fingroup.fingroup]
G:1325 [binder, in mathcomp.fingroup.fingroup]
G:1326 [binder, in mathcomp.fingroup.fingroup]
G:1327 [binder, in mathcomp.fingroup.fingroup]
G:1328 [binder, in mathcomp.fingroup.fingroup]
G:1329 [binder, in mathcomp.fingroup.fingroup]
g:133 [binder, in mathcomp.field.galois]
G:133 [binder, in mathcomp.solvable.pgroup]
G:133 [binder, in mathcomp.solvable.frobenius]
G:133 [binder, in mathcomp.solvable.abelian]
G:133 [binder, in mathcomp.solvable.cyclic]
G:133 [binder, in mathcomp.solvable.nilpotent]
G:1330 [binder, in mathcomp.fingroup.fingroup]
G:1331 [binder, in mathcomp.fingroup.fingroup]
G:1332 [binder, in mathcomp.fingroup.fingroup]
G:134 [binder, in mathcomp.solvable.commutator]
G:134 [binder, in mathcomp.fingroup.automorphism]
G:134 [binder, in mathcomp.fingroup.gproduct]
G:134 [binder, in mathcomp.solvable.extremal]
G:134 [binder, in mathcomp.solvable.gseries]
G:134 [binder, in mathcomp.solvable.maximal]
G:135 [binder, in mathcomp.solvable.abelian]
G:135 [binder, in mathcomp.fingroup.morphism]
G:135 [binder, in mathcomp.solvable.hall]
G:135 [binder, in mathcomp.solvable.maximal]
G:1356 [binder, in mathcomp.algebra.ssralg]
G:136 [binder, in mathcomp.solvable.sylow]
G:136 [binder, in mathcomp.solvable.frobenius]
G:136 [binder, in mathcomp.solvable.gseries]
G:136 [binder, in mathcomp.solvable.cyclic]
G:136 [binder, in mathcomp.solvable.nilpotent]
G:137 [binder, in mathcomp.fingroup.gproduct]
G:137 [binder, in mathcomp.solvable.abelian]
G:137 [binder, in mathcomp.solvable.nilpotent]
G:138 [binder, in mathcomp.solvable.commutator]
G:138 [binder, in mathcomp.solvable.extremal]
g:139 [binder, in mathcomp.field.galois]
G:139 [binder, in mathcomp.solvable.sylow]
G:139 [binder, in mathcomp.solvable.pgroup]
G:139 [binder, in mathcomp.solvable.gseries]
G:139 [binder, in mathcomp.fingroup.morphism]
G:139 [binder, in mathcomp.solvable.cyclic]
G:139 [binder, in mathcomp.solvable.hall]
G:14 [binder, in mathcomp.fingroup.fingroup]
G:14 [binder, in mathcomp.solvable.center]
G:14 [binder, in mathcomp.solvable.nilpotent]
G:140 [binder, in mathcomp.solvable.commutator]
g:140 [binder, in mathcomp.field.galois]
G:140 [binder, in mathcomp.solvable.frobenius]
G:140 [binder, in mathcomp.fingroup.gproduct]
G:140 [binder, in mathcomp.solvable.abelian]
g:1403 [binder, in mathcomp.algebra.matrix]
G:141 [binder, in mathcomp.solvable.sylow]
G:141 [binder, in mathcomp.solvable.pgroup]
G:141 [binder, in mathcomp.solvable.cyclic]
G:141 [binder, in mathcomp.solvable.nilpotent]
g:1416 [binder, in mathcomp.ssreflect.seq]
G:142 [binder, in mathcomp.solvable.commutator]
G:142 [binder, in mathcomp.fingroup.automorphism]
G:142 [binder, in mathcomp.solvable.abelian]
G:142 [binder, in mathcomp.solvable.gseries]
G:143 [binder, in mathcomp.solvable.cyclic]
G:144 [binder, in mathcomp.character.integral_char]
G:144 [binder, in mathcomp.solvable.commutator]
G:144 [binder, in mathcomp.solvable.sylow]
G:144 [binder, in mathcomp.solvable.pgroup]
G:144 [binder, in mathcomp.solvable.frobenius]
G:144 [binder, in mathcomp.fingroup.gproduct]
G:144 [binder, in mathcomp.fingroup.morphism]
G:144 [binder, in mathcomp.solvable.hall]
G:1440 [binder, in mathcomp.character.mxrepresentation]
G:145 [binder, in mathcomp.solvable.sylow]
G:146 [binder, in mathcomp.solvable.commutator]
G:146 [binder, in mathcomp.solvable.gseries]
G:146 [binder, in mathcomp.solvable.nilpotent]
G:147 [binder, in mathcomp.solvable.sylow]
G:147 [binder, in mathcomp.solvable.pgroup]
G:147 [binder, in mathcomp.solvable.frobenius]
G:147 [binder, in mathcomp.fingroup.gproduct]
G:147 [binder, in mathcomp.solvable.abelian]
G:148 [binder, in mathcomp.solvable.commutator]
G:149 [binder, in mathcomp.fingroup.quotient]
G:149 [binder, in mathcomp.fingroup.automorphism]
G:149 [binder, in mathcomp.solvable.gseries]
G:15 [binder, in mathcomp.solvable.sylow]
g:15 [binder, in mathcomp.algebra.rat]
G:15 [binder, in mathcomp.solvable.maximal]
G:15 [binder, in mathcomp.solvable.nilpotent]
g:150 [binder, in mathcomp.character.integral_char]
G:150 [binder, in mathcomp.solvable.commutator]
G:150 [binder, in mathcomp.solvable.pgroup]
G:150 [binder, in mathcomp.solvable.frobenius]
G:151 [binder, in mathcomp.fingroup.quotient]
G:151 [binder, in mathcomp.fingroup.gproduct]
G:151 [binder, in mathcomp.solvable.abelian]
G:151 [binder, in mathcomp.solvable.center]
G:153 [binder, in mathcomp.solvable.frobenius]
G:153 [binder, in mathcomp.solvable.abelian]
G:153 [binder, in mathcomp.solvable.gseries]
g:1533 [binder, in mathcomp.algebra.mxalgebra]
g:1535 [binder, in mathcomp.algebra.mxalgebra]
g:1537 [binder, in mathcomp.algebra.mxalgebra]
G:154 [binder, in mathcomp.fingroup.gproduct]
G:154 [binder, in mathcomp.solvable.abelian]
G:155 [binder, in mathcomp.solvable.finmodule]
G:155 [binder, in mathcomp.solvable.commutator]
G:155 [binder, in mathcomp.solvable.cyclic]
G:155 [binder, in mathcomp.solvable.nilpotent]
g:1554 [binder, in mathcomp.character.mxrepresentation]
g:1557 [binder, in mathcomp.character.mxrepresentation]
G:156 [binder, in mathcomp.solvable.pgroup]
G:156 [binder, in mathcomp.solvable.gseries]
G:156 [binder, in mathcomp.fingroup.morphism]
g:1561 [binder, in mathcomp.character.mxrepresentation]
g:1565 [binder, in mathcomp.character.mxrepresentation]
G:157 [binder, in mathcomp.solvable.commutator]
g:157 [binder, in mathcomp.character.mxrepresentation]
G:158 [binder, in mathcomp.fingroup.gproduct]
G:158 [binder, in mathcomp.solvable.gseries]
G:160 [binder, in mathcomp.solvable.commutator]
G:160 [binder, in mathcomp.solvable.pgroup]
G:160 [binder, in mathcomp.solvable.nilpotent]
G:161 [binder, in mathcomp.solvable.sylow]
G:161 [binder, in mathcomp.solvable.gseries]
G:161 [binder, in mathcomp.fingroup.morphism]
g:1610 [binder, in mathcomp.ssreflect.seq]
g:1611 [binder, in mathcomp.algebra.matrix]
G:162 [binder, in mathcomp.fingroup.quotient]
G:162 [binder, in mathcomp.solvable.commutator]
G:162 [binder, in mathcomp.solvable.nilpotent]
g:1625 [binder, in mathcomp.algebra.matrix]
G:163 [binder, in mathcomp.solvable.sylow]
G:1635 [binder, in mathcomp.character.mxrepresentation]
G:164 [binder, in mathcomp.solvable.sylow]
G:164 [binder, in mathcomp.solvable.pgroup]
G:164 [binder, in mathcomp.solvable.frobenius]
G:164 [binder, in mathcomp.solvable.nilpotent]
G:165 [binder, in mathcomp.solvable.commutator]
G:165 [binder, in mathcomp.solvable.gseries]
G:165 [binder, in mathcomp.fingroup.morphism]
G:1650 [binder, in mathcomp.character.mxrepresentation]
G:1653 [binder, in mathcomp.algebra.ssrnum]
G:1654 [binder, in mathcomp.algebra.ssrnum]
G:1655 [binder, in mathcomp.algebra.ssrnum]
G:1657 [binder, in mathcomp.algebra.ssrnum]
g:1659 [binder, in mathcomp.ssreflect.seq]
G:166 [binder, in mathcomp.fingroup.gproduct]
G:166 [binder, in mathcomp.fingroup.morphism]
g:166 [binder, in mathcomp.character.character]
g:1666 [binder, in mathcomp.algebra.ssralg]
G:167 [binder, in mathcomp.fingroup.morphism]
G:167 [binder, in mathcomp.solvable.maximal]
G:168 [binder, in mathcomp.solvable.pgroup]
G:168 [binder, in mathcomp.solvable.maximal]
g:169 [binder, in mathcomp.algebra.matrix]
G:17 [binder, in mathcomp.solvable.sylow]
G:17 [binder, in mathcomp.solvable.frobenius]
G:17 [binder, in mathcomp.solvable.hall]
G:17 [binder, in mathcomp.solvable.gfunctor]
G:170 [binder, in mathcomp.solvable.pgroup]
G:170 [binder, in mathcomp.solvable.maximal]
g:172 [binder, in mathcomp.character.mxabelem]
G:172 [binder, in mathcomp.solvable.sylow]
G:172 [binder, in mathcomp.fingroup.gproduct]
G:173 [binder, in mathcomp.solvable.commutator]
G:173 [binder, in mathcomp.solvable.maximal]
G:174 [binder, in mathcomp.solvable.pgroup]
G:174 [binder, in mathcomp.solvable.nilpotent]
g:175 [binder, in mathcomp.algebra.matrix]
G:176 [binder, in mathcomp.fingroup.quotient]
g:176 [binder, in mathcomp.solvable.finmodule]
g:176 [binder, in mathcomp.character.mxabelem]
G:176 [binder, in mathcomp.fingroup.gproduct]
G:177 [binder, in mathcomp.fingroup.quotient]
g:177 [binder, in mathcomp.character.mxabelem]
G:177 [binder, in mathcomp.solvable.maximal]
G:177 [binder, in mathcomp.solvable.nilpotent]
G:178 [binder, in mathcomp.character.integral_char]
g:178 [binder, in mathcomp.algebra.matrix]
G:178 [binder, in mathcomp.solvable.pgroup]
G:179 [binder, in mathcomp.solvable.maximal]
G:179 [binder, in mathcomp.solvable.nilpotent]
G:180 [binder, in mathcomp.fingroup.gproduct]
g:181 [binder, in mathcomp.algebra.matrix]
G:181 [binder, in mathcomp.solvable.pgroup]
G:181 [binder, in mathcomp.solvable.nilpotent]
g:182 [binder, in mathcomp.solvable.finmodule]
G:183 [binder, in mathcomp.fingroup.gproduct]
G:183 [binder, in mathcomp.solvable.abelian]
G:183 [binder, in mathcomp.solvable.nilpotent]
G:1830 [binder, in mathcomp.algebra.ssrnum]
g:184 [binder, in mathcomp.algebra.matrix]
G:184 [binder, in mathcomp.solvable.nilpotent]
G:185 [binder, in mathcomp.solvable.pgroup]
G:186 [binder, in mathcomp.fingroup.action]
G:186 [binder, in mathcomp.solvable.nilpotent]
G:187 [binder, in mathcomp.fingroup.action]
G:187 [binder, in mathcomp.solvable.frobenius]
g:188 [binder, in mathcomp.algebra.matrix]
G:189 [binder, in mathcomp.fingroup.gproduct]
g:1894 [binder, in mathcomp.algebra.mxalgebra]
g:1897 [binder, in mathcomp.algebra.mxalgebra]
G:19 [binder, in mathcomp.fingroup.fingroup]
G:19 [binder, in mathcomp.solvable.sylow]
G:19 [binder, in mathcomp.solvable.gseries]
G:19 [binder, in mathcomp.solvable.nilpotent]
G:190 [binder, in mathcomp.solvable.pgroup]
G:191 [binder, in mathcomp.fingroup.action]
G:192 [binder, in mathcomp.character.integral_char]
g:192 [binder, in mathcomp.algebra.matrix]
G:193 [binder, in mathcomp.solvable.nilpotent]
G:194 [binder, in mathcomp.fingroup.action]
G:194 [binder, in mathcomp.solvable.pgroup]
G:194 [binder, in mathcomp.fingroup.gproduct]
g:1943 [binder, in mathcomp.algebra.matrix]
g:1945 [binder, in mathcomp.algebra.matrix]
g:1947 [binder, in mathcomp.algebra.matrix]
G:195 [binder, in mathcomp.fingroup.action]
g:1954 [binder, in mathcomp.algebra.matrix]
g:1957 [binder, in mathcomp.algebra.matrix]
g:196 [binder, in mathcomp.algebra.matrix]
G:196 [binder, in mathcomp.fingroup.action]
g:1969 [binder, in mathcomp.algebra.matrix]
g:197 [binder, in mathcomp.character.classfun]
G:197 [binder, in mathcomp.solvable.pgroup]
g:1972 [binder, in mathcomp.algebra.matrix]
g:1975 [binder, in mathcomp.algebra.matrix]
G:199 [binder, in mathcomp.character.integral_char]
G:199 [binder, in mathcomp.fingroup.action]
G:199 [binder, in mathcomp.solvable.nilpotent]
G:2 [binder, in mathcomp.character.integral_char]
G:2 [binder, in mathcomp.character.classfun]
g:2 [binder, in mathcomp.ssreflect.fingraph]
G:2 [binder, in mathcomp.solvable.hall]
G:20 [binder, in mathcomp.character.classfun]
G:20 [binder, in mathcomp.solvable.frobenius]
g:200 [binder, in mathcomp.algebra.matrix]
G:200 [binder, in mathcomp.solvable.pgroup]
G:201 [binder, in mathcomp.solvable.pgroup]
G:201 [binder, in mathcomp.fingroup.morphism]
G:202 [binder, in mathcomp.solvable.pgroup]
G:202 [binder, in mathcomp.solvable.extremal]
G:203 [binder, in mathcomp.fingroup.quotient]
G:203 [binder, in mathcomp.fingroup.morphism]
g:2033 [binder, in mathcomp.algebra.matrix]
G:204 [binder, in mathcomp.fingroup.gproduct]
g:2040 [binder, in mathcomp.algebra.matrix]
g:205 [binder, in mathcomp.fingroup.quotient]
G:205 [binder, in mathcomp.fingroup.action]
G:205 [binder, in mathcomp.fingroup.gproduct]
G:205 [binder, in mathcomp.solvable.maximal]
G:205 [binder, in mathcomp.solvable.nilpotent]
g:206 [binder, in mathcomp.fingroup.quotient]
G:206 [binder, in mathcomp.solvable.maximal]
g:2061 [binder, in mathcomp.algebra.matrix]
G:207 [binder, in mathcomp.fingroup.gproduct]
G:207 [binder, in mathcomp.solvable.maximal]
G:208 [binder, in mathcomp.fingroup.action]
G:209 [binder, in mathcomp.solvable.abelian]
G:209 [binder, in mathcomp.solvable.maximal]
G:21 [binder, in mathcomp.solvable.center]
G:211 [binder, in mathcomp.solvable.pgroup]
G:211 [binder, in mathcomp.fingroup.gproduct]
g:2112 [binder, in mathcomp.ssreflect.seq]
g:212 [binder, in mathcomp.fingroup.quotient]
G:212 [binder, in mathcomp.character.mxabelem]
G:212 [binder, in mathcomp.solvable.maximal]
G:2123 [binder, in mathcomp.ssreflect.bigop]
g:2125 [binder, in mathcomp.ssreflect.seq]
g:213 [binder, in mathcomp.fingroup.quotient]
G:213 [binder, in mathcomp.solvable.cyclic]
G:214 [binder, in mathcomp.fingroup.gproduct]
G:214 [binder, in mathcomp.solvable.maximal]
g:2140 [binder, in mathcomp.ssreflect.seq]
G:216 [binder, in mathcomp.solvable.maximal]
G:217 [binder, in mathcomp.fingroup.gproduct]
G:217 [binder, in mathcomp.solvable.nilpotent]
G:218 [binder, in mathcomp.solvable.maximal]
G:22 [binder, in mathcomp.fingroup.fingroup]
G:22 [binder, in mathcomp.solvable.gfunctor]
g:22 [binder, in mathcomp.ssreflect.ssrfun]
G:22 [binder, in mathcomp.solvable.nilpotent]
G:220 [binder, in mathcomp.fingroup.gproduct]
G:224 [binder, in mathcomp.fingroup.action]
g:2247 [binder, in mathcomp.ssreflect.seq]
G:225 [binder, in mathcomp.solvable.nilpotent]
G:226 [binder, in mathcomp.fingroup.action]
G:226 [binder, in mathcomp.fingroup.gproduct]
G:227 [binder, in mathcomp.character.integral_char]
G:227 [binder, in mathcomp.solvable.nilpotent]
g:2274 [binder, in mathcomp.algebra.matrix]
G:228 [binder, in mathcomp.fingroup.action]
g:2281 [binder, in mathcomp.algebra.matrix]
g:2287 [binder, in mathcomp.algebra.matrix]
g:2290 [binder, in mathcomp.algebra.matrix]
G:23 [binder, in mathcomp.solvable.jordanholder]
G:23 [binder, in mathcomp.solvable.pgroup]
G:23 [binder, in mathcomp.solvable.center]
G:230 [binder, in mathcomp.solvable.nilpotent]
G:231 [binder, in mathcomp.fingroup.gproduct]
G:232 [binder, in mathcomp.solvable.nilpotent]
G:234 [binder, in mathcomp.fingroup.quotient]
G:234 [binder, in mathcomp.fingroup.action]
G:234 [binder, in mathcomp.solvable.nilpotent]
g:235 [binder, in mathcomp.character.classfun]
G:236 [binder, in mathcomp.solvable.nilpotent]
G:2360 [binder, in mathcomp.algebra.ssrnum]
g:237 [binder, in mathcomp.character.classfun]
g:238 [binder, in mathcomp.character.classfun]
g:239 [binder, in mathcomp.character.classfun]
G:24 [binder, in mathcomp.fingroup.fingroup]
G:24 [binder, in mathcomp.solvable.center]
G:24 [binder, in mathcomp.solvable.hall]
g:240 [binder, in mathcomp.character.classfun]
G:240 [binder, in mathcomp.solvable.abelian]
G:241 [binder, in mathcomp.fingroup.quotient]
G:241 [binder, in mathcomp.character.inertia]
g:241 [binder, in mathcomp.character.classfun]
G:242 [binder, in mathcomp.fingroup.quotient]
G:242 [binder, in mathcomp.fingroup.gproduct]
G:242 [binder, in mathcomp.solvable.nilpotent]
G:243 [binder, in mathcomp.solvable.abelian]
G:244 [binder, in mathcomp.fingroup.quotient]
G:244 [binder, in mathcomp.solvable.abelian]
G:244 [binder, in mathcomp.solvable.nilpotent]
G:245 [binder, in mathcomp.fingroup.quotient]
G:245 [binder, in mathcomp.solvable.nilpotent]
G:246 [binder, in mathcomp.solvable.nilpotent]
G:247 [binder, in mathcomp.fingroup.quotient]
G:247 [binder, in mathcomp.solvable.nilpotent]
G:248 [binder, in mathcomp.solvable.nilpotent]
G:249 [binder, in mathcomp.fingroup.quotient]
G:249 [binder, in mathcomp.fingroup.action]
G:249 [binder, in mathcomp.solvable.abelian]
g:249 [binder, in mathcomp.fingroup.morphism]
G:25 [binder, in mathcomp.solvable.gseries]
G:25 [binder, in mathcomp.solvable.center]
G:25 [binder, in mathcomp.solvable.gfunctor]
G:250 [binder, in mathcomp.character.inertia]
G:251 [binder, in mathcomp.fingroup.quotient]
G:252 [binder, in mathcomp.solvable.abelian]
G:252 [binder, in mathcomp.solvable.nilpotent]
G:253 [binder, in mathcomp.fingroup.quotient]
g:253 [binder, in mathcomp.fingroup.morphism]
G:253 [binder, in mathcomp.solvable.cyclic]
G:254 [binder, in mathcomp.solvable.nilpotent]
G:255 [binder, in mathcomp.fingroup.quotient]
G:255 [binder, in mathcomp.character.inertia]
G:256 [binder, in mathcomp.fingroup.gproduct]
G:256 [binder, in mathcomp.solvable.abelian]
G:257 [binder, in mathcomp.fingroup.action]
G:257 [binder, in mathcomp.solvable.nilpotent]
G:259 [binder, in mathcomp.character.inertia]
G:259 [binder, in mathcomp.solvable.nilpotent]
G:2597 [binder, in mathcomp.ssreflect.bigop]
G:26 [binder, in mathcomp.solvable.pgroup]
G:26 [binder, in mathcomp.solvable.nilpotent]
G:260 [binder, in mathcomp.fingroup.action]
G:260 [binder, in mathcomp.fingroup.gproduct]
G:261 [binder, in mathcomp.solvable.nilpotent]
G:262 [binder, in mathcomp.fingroup.quotient]
G:262 [binder, in mathcomp.fingroup.morphism]
G:262 [binder, in mathcomp.solvable.nilpotent]
g:263 [binder, in mathcomp.field.galois]
G:263 [binder, in mathcomp.character.inertia]
G:263 [binder, in mathcomp.fingroup.action]
g:263 [binder, in mathcomp.field.closed_field]
G:263 [binder, in mathcomp.fingroup.morphism]
G:263 [binder, in mathcomp.solvable.nilpotent]
G:267 [binder, in mathcomp.solvable.abelian]
G:267 [binder, in mathcomp.solvable.nilpotent]
g:268 [binder, in mathcomp.field.galois]
G:269 [binder, in mathcomp.solvable.nilpotent]
G:27 [binder, in mathcomp.solvable.center]
g:27 [binder, in mathcomp.ssreflect.ssrfun]
G:271 [binder, in mathcomp.fingroup.action]
G:271 [binder, in mathcomp.solvable.nilpotent]
G:273 [binder, in mathcomp.fingroup.action]
G:273 [binder, in mathcomp.solvable.nilpotent]
G:275 [binder, in mathcomp.fingroup.action]
G:275 [binder, in mathcomp.solvable.nilpotent]
G:276 [binder, in mathcomp.solvable.nilpotent]
g:277 [binder, in mathcomp.algebra.mxpoly]
G:277 [binder, in mathcomp.fingroup.gproduct]
G:277 [binder, in mathcomp.solvable.abelian]
G:278 [binder, in mathcomp.solvable.pgroup]
G:278 [binder, in mathcomp.solvable.nilpotent]
g:279 [binder, in mathcomp.fingroup.morphism]
G:279 [binder, in mathcomp.solvable.nilpotent]
G:28 [binder, in mathcomp.solvable.jordanholder]
G:28 [binder, in mathcomp.fingroup.gproduct]
G:28 [binder, in mathcomp.solvable.gseries]
g:28 [binder, in mathcomp.field.falgebra]
G:280 [binder, in mathcomp.solvable.nilpotent]
g:281 [binder, in mathcomp.algebra.mxpoly]
G:281 [binder, in mathcomp.solvable.abelian]
g:282 [binder, in mathcomp.field.galois]
G:282 [binder, in mathcomp.solvable.nilpotent]
g:283 [binder, in mathcomp.fingroup.morphism]
g:284 [binder, in mathcomp.algebra.mxpoly]
G:284 [binder, in mathcomp.solvable.nilpotent]
g:286 [binder, in mathcomp.algebra.mxpoly]
G:286 [binder, in mathcomp.fingroup.action]
g:287 [binder, in mathcomp.field.galois]
G:287 [binder, in mathcomp.solvable.pgroup]
G:287 [binder, in mathcomp.solvable.abelian]
g:288 [binder, in mathcomp.algebra.mxpoly]
G:289 [binder, in mathcomp.fingroup.gproduct]
g:290 [binder, in mathcomp.field.closed_field]
g:2913 [binder, in mathcomp.algebra.ssralg]
g:292 [binder, in mathcomp.algebra.mxpoly]
G:294 [binder, in mathcomp.solvable.pgroup]
G:294 [binder, in mathcomp.fingroup.morphism]
G:294 [binder, in mathcomp.solvable.nilpotent]
g:2944 [binder, in mathcomp.algebra.ssralg]
g:295 [binder, in mathcomp.algebra.mxpoly]
G:296 [binder, in mathcomp.solvable.abelian]
G:296 [binder, in mathcomp.fingroup.morphism]
G:296 [binder, in mathcomp.solvable.nilpotent]
G:298 [binder, in mathcomp.solvable.abelian]
G:298 [binder, in mathcomp.solvable.nilpotent]
g:299 [binder, in mathcomp.algebra.mxpoly]
G:3 [binder, in mathcomp.character.classfun]
G:3 [binder, in mathcomp.character.mxrepresentation]
G:3 [binder, in mathcomp.solvable.center]
G:3 [binder, in mathcomp.solvable.burnside_app]
G:3 [binder, in mathcomp.solvable.maximal]
G:30 [binder, in mathcomp.solvable.jordanholder]
G:30 [binder, in mathcomp.solvable.cyclic]
G:300 [binder, in mathcomp.solvable.nilpotent]
G:301 [binder, in mathcomp.solvable.pgroup]
g:305 [binder, in mathcomp.algebra.mxpoly]
G:307 [binder, in mathcomp.solvable.pgroup]
G:308 [binder, in mathcomp.solvable.abelian]
G:31 [binder, in mathcomp.fingroup.gproduct]
g:31 [binder, in mathcomp.field.falgebra]
G:311 [binder, in mathcomp.solvable.pgroup]
g:312 [binder, in mathcomp.field.galois]
G:312 [binder, in mathcomp.fingroup.gproduct]
G:312 [binder, in mathcomp.solvable.abelian]
G:313 [binder, in mathcomp.fingroup.action]
G:315 [binder, in mathcomp.fingroup.action]
G:316 [binder, in mathcomp.solvable.abelian]
G:317 [binder, in mathcomp.fingroup.action]
G:317 [binder, in mathcomp.solvable.pgroup]
G:319 [binder, in mathcomp.solvable.pgroup]
G:32 [binder, in mathcomp.fingroup.fingroup]
G:32 [binder, in mathcomp.solvable.cyclic]
G:320 [binder, in mathcomp.fingroup.action]
G:320 [binder, in mathcomp.solvable.abelian]
g:321 [binder, in mathcomp.algebra.mxpoly]
G:321 [binder, in mathcomp.solvable.pgroup]
G:321 [binder, in mathcomp.solvable.abelian]
g:322 [binder, in mathcomp.character.vcharacter]
G:322 [binder, in mathcomp.solvable.abelian]
G:326 [binder, in mathcomp.fingroup.action]
G:326 [binder, in mathcomp.fingroup.gproduct]
G:327 [binder, in mathcomp.fingroup.gproduct]
G:328 [binder, in mathcomp.fingroup.action]
G:328 [binder, in mathcomp.solvable.abelian]
G:329 [binder, in mathcomp.fingroup.gproduct]
G:33 [binder, in mathcomp.solvable.frobenius]
g:33 [binder, in mathcomp.ssreflect.ssrfun]
G:33 [binder, in mathcomp.solvable.maximal]
G:33 [binder, in mathcomp.solvable.nilpotent]
G:330 [binder, in mathcomp.solvable.abelian]
G:330 [binder, in mathcomp.character.character]
g:332 [binder, in mathcomp.field.falgebra]
G:333 [binder, in mathcomp.solvable.pgroup]
G:333 [binder, in mathcomp.solvable.abelian]
g:334 [binder, in mathcomp.field.falgebra]
G:335 [binder, in mathcomp.character.character]
g:337 [binder, in mathcomp.algebra.mxpoly]
G:337 [binder, in mathcomp.fingroup.gproduct]
G:338 [binder, in mathcomp.solvable.pgroup]
G:34 [binder, in mathcomp.fingroup.quotient]
g:34 [binder, in mathcomp.ssreflect.finfun]
G:34 [binder, in mathcomp.solvable.jordanholder]
G:34 [binder, in mathcomp.solvable.extremal]
G:34 [binder, in mathcomp.solvable.cyclic]
G:34 [binder, in mathcomp.solvable.maximal]
g:340 [binder, in mathcomp.algebra.mxpoly]
G:340 [binder, in mathcomp.fingroup.gproduct]
G:342 [binder, in mathcomp.solvable.pgroup]
g:343 [binder, in mathcomp.algebra.mxpoly]
G:343 [binder, in mathcomp.fingroup.gproduct]
G:343 [binder, in mathcomp.solvable.abelian]
g:344 [binder, in mathcomp.ssreflect.eqtype]
g:345 [binder, in mathcomp.ssreflect.eqtype]
G:346 [binder, in mathcomp.fingroup.gproduct]
g:347 [binder, in mathcomp.algebra.mxpoly]
G:347 [binder, in mathcomp.fingroup.action]
G:349 [binder, in mathcomp.solvable.pgroup]
G:349 [binder, in mathcomp.fingroup.gproduct]
G:349 [binder, in mathcomp.solvable.abelian]
g:35 [binder, in mathcomp.character.integral_char]
G:35 [binder, in mathcomp.solvable.gseries]
G:35 [binder, in mathcomp.solvable.hall]
G:350 [binder, in mathcomp.fingroup.action]
G:350 [binder, in mathcomp.fingroup.gproduct]
g:352 [binder, in mathcomp.ssreflect.eqtype]
g:352 [binder, in mathcomp.field.falgebra]
g:354 [binder, in mathcomp.algebra.mxpoly]
G:354 [binder, in mathcomp.fingroup.action]
G:354 [binder, in mathcomp.solvable.pgroup]
G:354 [binder, in mathcomp.solvable.abelian]
g:354 [binder, in mathcomp.ssreflect.eqtype]
g:354 [binder, in mathcomp.field.falgebra]
G:356 [binder, in mathcomp.solvable.abelian]
g:357 [binder, in mathcomp.algebra.mxpoly]
G:357 [binder, in mathcomp.fingroup.action]
g:357 [binder, in mathcomp.ssreflect.eqtype]
G:358 [binder, in mathcomp.fingroup.gproduct]
g:359 [binder, in mathcomp.algebra.matrix]
g:359 [binder, in mathcomp.ssreflect.eqtype]
G:36 [binder, in mathcomp.solvable.jordanholder]
G:36 [binder, in mathcomp.solvable.gseries]
G:36 [binder, in mathcomp.solvable.maximal]
G:360 [binder, in mathcomp.solvable.abelian]
G:361 [binder, in mathcomp.fingroup.action]
G:362 [binder, in mathcomp.solvable.pgroup]
G:363 [binder, in mathcomp.solvable.pgroup]
G:363 [binder, in mathcomp.fingroup.gproduct]
G:364 [binder, in mathcomp.fingroup.action]
G:364 [binder, in mathcomp.solvable.abelian]
G:365 [binder, in mathcomp.solvable.pgroup]
g:366 [binder, in mathcomp.algebra.mxpoly]
G:367 [binder, in mathcomp.solvable.pgroup]
G:368 [binder, in mathcomp.fingroup.action]
G:368 [binder, in mathcomp.fingroup.gproduct]
G:37 [binder, in mathcomp.solvable.cyclic]
G:37 [binder, in mathcomp.solvable.maximal]
G:370 [binder, in mathcomp.solvable.pgroup]
g:372 [binder, in mathcomp.algebra.mxpoly]
g:373 [binder, in mathcomp.algebra.matrix]
G:373 [binder, in mathcomp.solvable.pgroup]
G:373 [binder, in mathcomp.solvable.extremal]
g:375 [binder, in mathcomp.algebra.mxpoly]
G:375 [binder, in mathcomp.solvable.pgroup]
g:378 [binder, in mathcomp.algebra.mxpoly]
g:378 [binder, in mathcomp.character.inertia]
G:378 [binder, in mathcomp.solvable.pgroup]
G:379 [binder, in mathcomp.fingroup.gproduct]
G:38 [binder, in mathcomp.fingroup.gproduct]
G:38 [binder, in mathcomp.solvable.center]
G:38 [binder, in mathcomp.solvable.hall]
G:38 [binder, in mathcomp.solvable.nilpotent]
g:381 [binder, in mathcomp.algebra.matrix]
G:381 [binder, in mathcomp.solvable.pgroup]
g:388 [binder, in mathcomp.algebra.matrix]
G:39 [binder, in mathcomp.solvable.jordanholder]
G:39 [binder, in mathcomp.solvable.gseries]
g:39 [binder, in mathcomp.ssreflect.ssrfun]
G:390 [binder, in mathcomp.fingroup.gproduct]
g:394 [binder, in mathcomp.character.inertia]
G:394 [binder, in mathcomp.solvable.abelian]
g:395 [binder, in mathcomp.character.inertia]
G:395 [binder, in mathcomp.solvable.extremal]
g:396 [binder, in mathcomp.character.inertia]
G:396 [binder, in mathcomp.fingroup.action]
g:397 [binder, in mathcomp.character.inertia]
g:398 [binder, in mathcomp.character.inertia]
G:4 [binder, in mathcomp.solvable.gfunctor]
g:40 [binder, in mathcomp.ssreflect.finfun]
g:40 [binder, in mathcomp.character.mxrepresentation]
G:40 [binder, in mathcomp.solvable.center]
G:40 [binder, in mathcomp.solvable.cyclic]
G:40 [binder, in mathcomp.solvable.maximal]
G:40 [binder, in mathcomp.solvable.nilpotent]
g:40 [binder, in mathcomp.field.falgebra]
G:401 [binder, in mathcomp.fingroup.action]
G:401 [binder, in mathcomp.solvable.abelian]
G:402 [binder, in mathcomp.solvable.pgroup]
G:403 [binder, in mathcomp.fingroup.action]
G:403 [binder, in mathcomp.solvable.pgroup]
G:403 [binder, in mathcomp.solvable.abelian]
G:404 [binder, in mathcomp.solvable.pgroup]
G:405 [binder, in mathcomp.fingroup.action]
G:405 [binder, in mathcomp.solvable.pgroup]
G:406 [binder, in mathcomp.solvable.pgroup]
G:406 [binder, in mathcomp.solvable.abelian]
g:407 [binder, in mathcomp.character.inertia]
G:407 [binder, in mathcomp.solvable.pgroup]
g:408 [binder, in mathcomp.character.inertia]
G:408 [binder, in mathcomp.solvable.abelian]
g:409 [binder, in mathcomp.character.inertia]
G:41 [binder, in mathcomp.fingroup.quotient]
G:41 [binder, in mathcomp.solvable.jordanholder]
g:41 [binder, in mathcomp.character.mxrepresentation]
G:41 [binder, in mathcomp.fingroup.gproduct]
G:41 [binder, in mathcomp.solvable.extraspecial]
g:410 [binder, in mathcomp.character.inertia]
g:411 [binder, in mathcomp.character.inertia]
G:411 [binder, in mathcomp.solvable.extremal]
G:412 [binder, in mathcomp.fingroup.gproduct]
G:414 [binder, in mathcomp.solvable.abelian]
G:416 [binder, in mathcomp.fingroup.action]
G:416 [binder, in mathcomp.fingroup.gproduct]
G:416 [binder, in mathcomp.solvable.abelian]
g:417 [binder, in mathcomp.character.inertia]
G:417 [binder, in mathcomp.solvable.pgroup]
g:418 [binder, in mathcomp.algebra.matrix]
g:418 [binder, in mathcomp.character.inertia]
g:419 [binder, in mathcomp.character.inertia]
G:419 [binder, in mathcomp.fingroup.action]
g:42 [binder, in mathcomp.character.mxrepresentation]
G:42 [binder, in mathcomp.solvable.gseries]
G:42 [binder, in mathcomp.solvable.nilpotent]
g:420 [binder, in mathcomp.character.inertia]
G:420 [binder, in mathcomp.fingroup.gproduct]
G:420 [binder, in mathcomp.solvable.abelian]
g:421 [binder, in mathcomp.character.inertia]
G:421 [binder, in mathcomp.solvable.abelian]
G:422 [binder, in mathcomp.solvable.extremal]
G:423 [binder, in mathcomp.solvable.pgroup]
G:424 [binder, in mathcomp.solvable.pgroup]
G:424 [binder, in mathcomp.fingroup.gproduct]
g:425 [binder, in mathcomp.algebra.matrix]
G:425 [binder, in mathcomp.fingroup.action]
G:425 [binder, in mathcomp.solvable.pgroup]
G:425 [binder, in mathcomp.solvable.abelian]
G:426 [binder, in mathcomp.solvable.abelian]
G:426 [binder, in mathcomp.character.character]
G:427 [binder, in mathcomp.fingroup.action]
G:427 [binder, in mathcomp.solvable.pgroup]
G:428 [binder, in mathcomp.solvable.abelian]
G:429 [binder, in mathcomp.solvable.pgroup]
G:429 [binder, in mathcomp.fingroup.gproduct]
G:43 [binder, in mathcomp.solvable.jordanholder]
G:43 [binder, in mathcomp.solvable.center]
G:43 [binder, in mathcomp.solvable.maximal]
G:430 [binder, in mathcomp.fingroup.action]
G:430 [binder, in mathcomp.solvable.pgroup]
G:430 [binder, in mathcomp.solvable.extremal]
G:431 [binder, in mathcomp.solvable.abelian]
G:432 [binder, in mathcomp.fingroup.action]
G:432 [binder, in mathcomp.solvable.pgroup]
G:432 [binder, in mathcomp.fingroup.morphism]
g:433 [binder, in mathcomp.algebra.matrix]
G:433 [binder, in mathcomp.solvable.pgroup]
G:433 [binder, in mathcomp.solvable.extremal]
G:433 [binder, in mathcomp.solvable.abelian]
G:435 [binder, in mathcomp.solvable.pgroup]
G:435 [binder, in mathcomp.solvable.abelian]
G:436 [binder, in mathcomp.character.inertia]
G:436 [binder, in mathcomp.solvable.extremal]
g:436 [binder, in mathcomp.algebra.ssralg]
G:437 [binder, in mathcomp.solvable.pgroup]
G:439 [binder, in mathcomp.fingroup.action]
G:44 [binder, in mathcomp.fingroup.gproduct]
g:44 [binder, in mathcomp.ssreflect.ssrbool]
G:44 [binder, in mathcomp.solvable.maximal]
G:44 [binder, in mathcomp.solvable.nilpotent]
G:440 [binder, in mathcomp.solvable.pgroup]
G:440 [binder, in mathcomp.fingroup.gproduct]
G:440 [binder, in mathcomp.solvable.abelian]
G:440 [binder, in mathcomp.fingroup.morphism]
G:441 [binder, in mathcomp.solvable.abelian]
G:442 [binder, in mathcomp.fingroup.action]
G:442 [binder, in mathcomp.solvable.pgroup]
G:443 [binder, in mathcomp.solvable.pgroup]
G:443 [binder, in mathcomp.fingroup.morphism]
G:444 [binder, in mathcomp.solvable.abelian]
g:445 [binder, in mathcomp.algebra.matrix]
G:447 [binder, in mathcomp.fingroup.action]
G:447 [binder, in mathcomp.solvable.abelian]
G:447 [binder, in mathcomp.fingroup.morphism]
G:448 [binder, in mathcomp.solvable.pgroup]
G:45 [binder, in mathcomp.solvable.gseries]
G:45 [binder, in mathcomp.solvable.center]
g:45 [binder, in mathcomp.ssreflect.ssrfun]
G:450 [binder, in mathcomp.solvable.abelian]
G:451 [binder, in mathcomp.fingroup.morphism]
G:452 [binder, in mathcomp.solvable.abelian]
G:453 [binder, in mathcomp.fingroup.gproduct]
G:455 [binder, in mathcomp.solvable.pgroup]
G:455 [binder, in mathcomp.solvable.abelian]
G:456 [binder, in mathcomp.fingroup.morphism]
G:457 [binder, in mathcomp.solvable.abelian]
G:459 [binder, in mathcomp.solvable.pgroup]
G:46 [binder, in mathcomp.solvable.nilpotent]
G:462 [binder, in mathcomp.solvable.pgroup]
G:462 [binder, in mathcomp.solvable.abelian]
G:462 [binder, in mathcomp.fingroup.morphism]
G:465 [binder, in mathcomp.character.inertia]
G:465 [binder, in mathcomp.fingroup.gproduct]
G:465 [binder, in mathcomp.solvable.abelian]
G:468 [binder, in mathcomp.solvable.pgroup]
G:47 [binder, in mathcomp.fingroup.quotient]
G:47 [binder, in mathcomp.solvable.center]
G:47 [binder, in mathcomp.solvable.hall]
G:47 [binder, in mathcomp.solvable.maximal]
G:476 [binder, in mathcomp.character.inertia]
G:476 [binder, in mathcomp.fingroup.gproduct]
G:478 [binder, in mathcomp.solvable.pgroup]
g:48 [binder, in mathcomp.character.integral_char]
G:48 [binder, in mathcomp.solvable.gseries]
G:48 [binder, in mathcomp.solvable.nilpotent]
G:482 [binder, in mathcomp.solvable.abelian]
G:483 [binder, in mathcomp.character.inertia]
g:4845 [binder, in mathcomp.ssreflect.order]
G:485 [binder, in mathcomp.solvable.abelian]
G:487 [binder, in mathcomp.solvable.abelian]
G:489 [binder, in mathcomp.solvable.abelian]
G:49 [binder, in mathcomp.solvable.center]
G:492 [binder, in mathcomp.solvable.pgroup]
G:492 [binder, in mathcomp.solvable.abelian]
G:494 [binder, in mathcomp.solvable.abelian]
G:495 [binder, in mathcomp.solvable.pgroup]
G:496 [binder, in mathcomp.character.inertia]
G:496 [binder, in mathcomp.solvable.abelian]
G:498 [binder, in mathcomp.solvable.pgroup]
G:5 [binder, in mathcomp.character.classfun]
G:5 [binder, in mathcomp.solvable.maximal]
G:50 [binder, in mathcomp.solvable.gseries]
g:50 [binder, in mathcomp.ssreflect.ssrbool]
G:50 [binder, in mathcomp.solvable.center]
G:50 [binder, in mathcomp.solvable.maximal]
G:50 [binder, in mathcomp.solvable.nilpotent]
G:500 [binder, in mathcomp.solvable.abelian]
G:502 [binder, in mathcomp.solvable.pgroup]
G:504 [binder, in mathcomp.fingroup.gproduct]
G:505 [binder, in mathcomp.solvable.abelian]
G:506 [binder, in mathcomp.solvable.pgroup]
G:507 [binder, in mathcomp.solvable.abelian]
G:508 [binder, in mathcomp.fingroup.action]
G:509 [binder, in mathcomp.character.inertia]
G:509 [binder, in mathcomp.solvable.abelian]
G:51 [binder, in mathcomp.solvable.jordanholder]
G:51 [binder, in mathcomp.solvable.pgroup]
G:51 [binder, in mathcomp.solvable.gseries]
G:510 [binder, in mathcomp.solvable.pgroup]
G:511 [binder, in mathcomp.solvable.abelian]
G:512 [binder, in mathcomp.solvable.abelian]
G:514 [binder, in mathcomp.solvable.pgroup]
G:514 [binder, in mathcomp.solvable.abelian]
G:515 [binder, in mathcomp.fingroup.gproduct]
G:515 [binder, in mathcomp.solvable.abelian]
G:517 [binder, in mathcomp.solvable.abelian]
G:518 [binder, in mathcomp.solvable.pgroup]
G:52 [binder, in mathcomp.fingroup.quotient]
G:52 [binder, in mathcomp.solvable.pgroup]
G:52 [binder, in mathcomp.solvable.center]
G:52 [binder, in mathcomp.solvable.hall]
G:52 [binder, in mathcomp.solvable.maximal]
G:52 [binder, in mathcomp.solvable.nilpotent]
G:521 [binder, in mathcomp.solvable.abelian]
G:522 [binder, in mathcomp.fingroup.action]
G:522 [binder, in mathcomp.solvable.pgroup]
G:525 [binder, in mathcomp.fingroup.action]
G:525 [binder, in mathcomp.fingroup.gproduct]
G:526 [binder, in mathcomp.solvable.pgroup]
G:526 [binder, in mathcomp.solvable.abelian]
G:528 [binder, in mathcomp.solvable.abelian]
G:53 [binder, in mathcomp.solvable.extraspecial]
G:530 [binder, in mathcomp.solvable.pgroup]
G:530 [binder, in mathcomp.solvable.abelian]
G:531 [binder, in mathcomp.solvable.abelian]
G:532 [binder, in mathcomp.character.inertia]
G:533 [binder, in mathcomp.solvable.abelian]
G:534 [binder, in mathcomp.solvable.pgroup]
G:535 [binder, in mathcomp.solvable.abelian]
G:538 [binder, in mathcomp.character.inertia]
G:538 [binder, in mathcomp.solvable.pgroup]
G:538 [binder, in mathcomp.solvable.abelian]
g:54 [binder, in mathcomp.ssreflect.finfun]
G:54 [binder, in mathcomp.solvable.pgroup]
G:54 [binder, in mathcomp.solvable.gseries]
G:54 [binder, in mathcomp.solvable.nilpotent]
G:540 [binder, in mathcomp.solvable.abelian]
G:542 [binder, in mathcomp.solvable.pgroup]
G:542 [binder, in mathcomp.solvable.abelian]
G:546 [binder, in mathcomp.solvable.pgroup]
G:547 [binder, in mathcomp.solvable.abelian]
G:55 [binder, in mathcomp.solvable.maximal]
G:550 [binder, in mathcomp.solvable.pgroup]
G:553 [binder, in mathcomp.solvable.pgroup]
G:555 [binder, in mathcomp.fingroup.fingroup]
G:557 [binder, in mathcomp.solvable.abelian]
G:558 [binder, in mathcomp.fingroup.fingroup]
G:558 [binder, in mathcomp.solvable.pgroup]
G:56 [binder, in mathcomp.solvable.pgroup]
G:56 [binder, in mathcomp.solvable.maximal]
G:562 [binder, in mathcomp.fingroup.fingroup]
G:562 [binder, in mathcomp.solvable.pgroup]
G:565 [binder, in mathcomp.fingroup.fingroup]
G:566 [binder, in mathcomp.fingroup.fingroup]
G:566 [binder, in mathcomp.solvable.pgroup]
G:566 [binder, in mathcomp.solvable.abelian]
G:567 [binder, in mathcomp.fingroup.fingroup]
G:57 [binder, in mathcomp.solvable.gseries]
G:57 [binder, in mathcomp.solvable.center]
G:57 [binder, in mathcomp.solvable.nilpotent]
G:570 [binder, in mathcomp.solvable.pgroup]
G:573 [binder, in mathcomp.solvable.pgroup]
G:574 [binder, in mathcomp.algebra.ssrnum]
G:576 [binder, in mathcomp.solvable.pgroup]
G:579 [binder, in mathcomp.solvable.pgroup]
g:58 [binder, in mathcomp.field.galois]
G:58 [binder, in mathcomp.solvable.hall]
G:581 [binder, in mathcomp.solvable.pgroup]
G:582 [binder, in mathcomp.solvable.abelian]
G:584 [binder, in mathcomp.solvable.pgroup]
G:585 [binder, in mathcomp.algebra.ssrnum]
G:587 [binder, in mathcomp.solvable.pgroup]
G:59 [binder, in mathcomp.ssreflect.finfun]
G:590 [binder, in mathcomp.solvable.pgroup]
G:593 [binder, in mathcomp.solvable.pgroup]
G:595 [binder, in mathcomp.solvable.pgroup]
G:597 [binder, in mathcomp.solvable.abelian]
G:6 [binder, in mathcomp.character.classfun]
G:6 [binder, in mathcomp.solvable.sylow]
G:6 [binder, in mathcomp.solvable.gfunctor]
G:6 [binder, in mathcomp.solvable.maximal]
G:60 [binder, in mathcomp.solvable.pgroup]
G:60 [binder, in mathcomp.solvable.center]
G:600 [binder, in mathcomp.solvable.abelian]
G:601 [binder, in mathcomp.solvable.pgroup]
G:601 [binder, in mathcomp.solvable.abelian]
g:603 [binder, in mathcomp.algebra.mxalgebra]
G:604 [binder, in mathcomp.solvable.pgroup]
g:606 [binder, in mathcomp.fingroup.action]
G:606 [binder, in mathcomp.solvable.abelian]
G:607 [binder, in mathcomp.solvable.pgroup]
G:61 [binder, in mathcomp.solvable.gseries]
G:610 [binder, in mathcomp.solvable.abelian]
g:611 [binder, in mathcomp.algebra.mxalgebra]
G:613 [binder, in mathcomp.solvable.abelian]
G:615 [binder, in mathcomp.fingroup.gproduct]
G:615 [binder, in mathcomp.solvable.abelian]
G:617 [binder, in mathcomp.solvable.abelian]
G:618 [binder, in mathcomp.solvable.abelian]
G:619 [binder, in mathcomp.solvable.pgroup]
G:62 [binder, in mathcomp.solvable.commutator]
G:62 [binder, in mathcomp.solvable.pgroup]
G:620 [binder, in mathcomp.solvable.abelian]
G:621 [binder, in mathcomp.solvable.abelian]
G:622 [binder, in mathcomp.solvable.pgroup]
G:622 [binder, in mathcomp.solvable.abelian]
G:624 [binder, in mathcomp.character.classfun]
G:624 [binder, in mathcomp.solvable.pgroup]
g:624 [binder, in mathcomp.algebra.mxalgebra]
G:626 [binder, in mathcomp.solvable.abelian]
g:628 [binder, in mathcomp.algebra.mxpoly]
G:63 [binder, in mathcomp.solvable.gseries]
G:63 [binder, in mathcomp.fingroup.presentation]
g:630 [binder, in mathcomp.algebra.mxpoly]
G:631 [binder, in mathcomp.solvable.abelian]
g:632 [binder, in mathcomp.algebra.mxalgebra]
G:635 [binder, in mathcomp.solvable.abelian]
G:638 [binder, in mathcomp.solvable.abelian]
G:64 [binder, in mathcomp.solvable.commutator]
G:64 [binder, in mathcomp.solvable.hall]
G:64 [binder, in mathcomp.solvable.nilpotent]
G:644 [binder, in mathcomp.fingroup.action]
G:65 [binder, in mathcomp.solvable.pgroup]
G:65 [binder, in mathcomp.solvable.maximal]
G:652 [binder, in mathcomp.solvable.abelian]
G:659 [binder, in mathcomp.solvable.abelian]
G:66 [binder, in mathcomp.solvable.commutator]
G:66 [binder, in mathcomp.solvable.gseries]
G:66 [binder, in mathcomp.fingroup.presentation]
g:660 [binder, in mathcomp.algebra.vector]
G:662 [binder, in mathcomp.solvable.abelian]
G:665 [binder, in mathcomp.field.galois]
g:665 [binder, in mathcomp.fingroup.fingroup]
G:666 [binder, in mathcomp.solvable.abelian]
G:668 [binder, in mathcomp.field.galois]
G:668 [binder, in mathcomp.solvable.abelian]
G:669 [binder, in mathcomp.solvable.abelian]
G:67 [binder, in mathcomp.solvable.pgroup]
G:67 [binder, in mathcomp.solvable.center]
G:67 [binder, in mathcomp.solvable.gfunctor]
G:670 [binder, in mathcomp.field.galois]
G:68 [binder, in mathcomp.solvable.commutator]
G:68 [binder, in mathcomp.solvable.cyclic]
G:68 [binder, in mathcomp.solvable.nilpotent]
g:683 [binder, in mathcomp.algebra.vector]
g:685 [binder, in mathcomp.algebra.vector]
g:689 [binder, in mathcomp.algebra.vector]
G:69 [binder, in mathcomp.solvable.pgroup]
G:69 [binder, in mathcomp.solvable.gfunctor]
g:694 [binder, in mathcomp.ssreflect.fintype]
g:696 [binder, in mathcomp.ssreflect.fintype]
g:698 [binder, in mathcomp.ssreflect.finset]
g:698 [binder, in mathcomp.ssreflect.fintype]
G:7 [binder, in mathcomp.solvable.maximal]
G:70 [binder, in mathcomp.solvable.hall]
g:701 [binder, in mathcomp.ssreflect.finset]
G:702 [binder, in mathcomp.fingroup.action]
g:704 [binder, in mathcomp.ssreflect.finset]
g:705 [binder, in mathcomp.ssreflect.fintype]
g:706 [binder, in mathcomp.ssreflect.fintype]
g:707 [binder, in mathcomp.ssreflect.finset]
g:708 [binder, in mathcomp.ssreflect.fintype]
G:71 [binder, in mathcomp.solvable.commutator]
G:71 [binder, in mathcomp.solvable.sylow]
G:71 [binder, in mathcomp.solvable.gseries]
g:713 [binder, in mathcomp.ssreflect.fintype]
g:715 [binder, in mathcomp.ssreflect.fintype]
G:717 [binder, in mathcomp.fingroup.gproduct]
G:72 [binder, in mathcomp.solvable.pgroup]
G:72 [binder, in mathcomp.solvable.center]
G:72 [binder, in mathcomp.solvable.cyclic]
G:72 [binder, in mathcomp.solvable.hall]
G:72 [binder, in mathcomp.solvable.nilpotent]
G:722 [binder, in mathcomp.fingroup.action]
g:723 [binder, in mathcomp.character.classfun]
G:724 [binder, in mathcomp.fingroup.action]
g:724 [binder, in mathcomp.character.classfun]
g:725 [binder, in mathcomp.character.classfun]
g:726 [binder, in mathcomp.character.classfun]
g:727 [binder, in mathcomp.character.classfun]
G:73 [binder, in mathcomp.fingroup.presentation]
G:73 [binder, in mathcomp.solvable.maximal]
g:730 [binder, in mathcomp.algebra.vector]
g:733 [binder, in mathcomp.algebra.vector]
g:734 [binder, in mathcomp.algebra.poly]
G:735 [binder, in mathcomp.fingroup.gproduct]
g:735 [binder, in mathcomp.algebra.poly]
G:737 [binder, in mathcomp.fingroup.action]
G:737 [binder, in mathcomp.fingroup.fingroup]
g:737 [binder, in mathcomp.algebra.vector]
G:739 [binder, in mathcomp.fingroup.action]
G:739 [binder, in mathcomp.fingroup.fingroup]
G:74 [binder, in mathcomp.solvable.commutator]
G:74 [binder, in mathcomp.solvable.sylow]
g:740 [binder, in mathcomp.algebra.poly]
G:741 [binder, in mathcomp.fingroup.fingroup]
g:741 [binder, in mathcomp.algebra.vector]
G:743 [binder, in mathcomp.fingroup.action]
G:743 [binder, in mathcomp.fingroup.fingroup]
G:745 [binder, in mathcomp.fingroup.fingroup]
g:746 [binder, in mathcomp.algebra.vector]
G:747 [binder, in mathcomp.fingroup.fingroup]
g:748 [binder, in mathcomp.algebra.vector]
G:749 [binder, in mathcomp.fingroup.fingroup]
G:75 [binder, in mathcomp.solvable.pgroup]
G:75 [binder, in mathcomp.solvable.extraspecial]
G:75 [binder, in mathcomp.solvable.maximal]
G:750 [binder, in mathcomp.character.character]
g:750 [binder, in mathcomp.algebra.poly]
G:751 [binder, in mathcomp.fingroup.fingroup]
G:755 [binder, in mathcomp.fingroup.fingroup]
g:755 [binder, in mathcomp.algebra.vector]
g:756 [binder, in mathcomp.algebra.poly]
G:758 [binder, in mathcomp.fingroup.fingroup]
g:758 [binder, in mathcomp.algebra.vector]
G:76 [binder, in mathcomp.solvable.commutator]
G:76 [binder, in mathcomp.solvable.gseries]
G:76 [binder, in mathcomp.solvable.hall]
G:76 [binder, in mathcomp.solvable.gfunctor]
G:76 [binder, in mathcomp.solvable.nilpotent]
G:760 [binder, in mathcomp.fingroup.fingroup]
G:762 [binder, in mathcomp.fingroup.fingroup]
G:77 [binder, in mathcomp.solvable.frobenius]
G:77 [binder, in mathcomp.solvable.abelian]
G:772 [binder, in mathcomp.fingroup.fingroup]
G:777 [binder, in mathcomp.character.classfun]
G:779 [binder, in mathcomp.fingroup.fingroup]
g:779 [binder, in mathcomp.algebra.vector]
G:78 [binder, in mathcomp.solvable.commutator]
G:78 [binder, in mathcomp.solvable.abelian]
G:782 [binder, in mathcomp.fingroup.fingroup]
g:79 [binder, in mathcomp.solvable.frobenius]
G:79 [binder, in mathcomp.solvable.abelian]
G:79 [binder, in mathcomp.solvable.center]
G:79 [binder, in mathcomp.solvable.gfunctor]
G:790 [binder, in mathcomp.fingroup.action]
g:793 [binder, in mathcomp.algebra.matrix]
G:793 [binder, in mathcomp.fingroup.action]
G:794 [binder, in mathcomp.fingroup.action]
G:795 [binder, in mathcomp.fingroup.action]
G:796 [binder, in mathcomp.fingroup.action]
G:797 [binder, in mathcomp.fingroup.action]
G:797 [binder, in mathcomp.character.mxrepresentation]
G:798 [binder, in mathcomp.fingroup.action]
G:799 [binder, in mathcomp.fingroup.action]
g:8 [binder, in mathcomp.ssreflect.finfun]
G:8 [binder, in mathcomp.character.classfun]
G:80 [binder, in mathcomp.character.integral_char]
G:80 [binder, in mathcomp.solvable.gseries]
G:80 [binder, in mathcomp.solvable.maximal]
G:800 [binder, in mathcomp.fingroup.action]
G:801 [binder, in mathcomp.character.mxrepresentation]
G:803 [binder, in mathcomp.character.mxrepresentation]
G:809 [binder, in mathcomp.fingroup.action]
G:81 [binder, in mathcomp.solvable.jordanholder]
G:81 [binder, in mathcomp.solvable.sylow]
G:81 [binder, in mathcomp.solvable.frobenius]
G:81 [binder, in mathcomp.solvable.abelian]
G:81 [binder, in mathcomp.solvable.gfunctor]
G:81 [binder, in mathcomp.solvable.extraspecial]
G:811 [binder, in mathcomp.fingroup.action]
g:813 [binder, in mathcomp.algebra.vector]
G:814 [binder, in mathcomp.fingroup.action]
G:817 [binder, in mathcomp.fingroup.action]
G:818 [binder, in mathcomp.fingroup.action]
G:82 [binder, in mathcomp.fingroup.quotient]
G:82 [binder, in mathcomp.solvable.commutator]
G:82 [binder, in mathcomp.solvable.center]
G:82 [binder, in mathcomp.solvable.hall]
G:82 [binder, in mathcomp.solvable.nilpotent]
G:820 [binder, in mathcomp.fingroup.action]
g:820 [binder, in mathcomp.algebra.ssralg]
G:822 [binder, in mathcomp.fingroup.action]
g:822 [binder, in mathcomp.algebra.vector]
G:824 [binder, in mathcomp.fingroup.action]
G:825 [binder, in mathcomp.fingroup.action]
G:825 [binder, in mathcomp.fingroup.fingroup]
g:825 [binder, in mathcomp.algebra.ssralg]
g:826 [binder, in mathcomp.algebra.vector]
G:826 [binder, in mathcomp.character.character]
G:827 [binder, in mathcomp.fingroup.fingroup]
G:829 [binder, in mathcomp.fingroup.action]
G:829 [binder, in mathcomp.fingroup.fingroup]
G:829 [binder, in mathcomp.character.character]
G:83 [binder, in mathcomp.solvable.pgroup]
G:83 [binder, in mathcomp.solvable.gseries]
G:83 [binder, in mathcomp.solvable.extraspecial]
G:83 [binder, in mathcomp.solvable.maximal]
G:830 [binder, in mathcomp.fingroup.action]
G:831 [binder, in mathcomp.fingroup.fingroup]
G:832 [binder, in mathcomp.fingroup.action]
G:832 [binder, in mathcomp.character.character]
G:833 [binder, in mathcomp.fingroup.fingroup]
g:835 [binder, in mathcomp.algebra.matrix]
G:835 [binder, in mathcomp.fingroup.fingroup]
G:835 [binder, in mathcomp.character.character]
G:838 [binder, in mathcomp.fingroup.fingroup]
g:838 [binder, in mathcomp.algebra.ssralg]
G:838 [binder, in mathcomp.character.character]
g:84 [binder, in mathcomp.solvable.frobenius]
G:84 [binder, in mathcomp.solvable.abelian]
G:84 [binder, in mathcomp.solvable.maximal]
G:840 [binder, in mathcomp.fingroup.action]
G:840 [binder, in mathcomp.fingroup.fingroup]
G:841 [binder, in mathcomp.character.character]
G:842 [binder, in mathcomp.fingroup.fingroup]
G:844 [binder, in mathcomp.fingroup.fingroup]
G:844 [binder, in mathcomp.character.character]
G:846 [binder, in mathcomp.fingroup.fingroup]
G:847 [binder, in mathcomp.character.character]
G:849 [binder, in mathcomp.fingroup.fingroup]
G:85 [binder, in mathcomp.fingroup.quotient]
G:85 [binder, in mathcomp.solvable.hall]
G:85 [binder, in mathcomp.solvable.gfunctor]
G:85 [binder, in mathcomp.solvable.maximal]
G:850 [binder, in mathcomp.character.character]
G:852 [binder, in mathcomp.fingroup.fingroup]
G:853 [binder, in mathcomp.character.character]
G:855 [binder, in mathcomp.fingroup.fingroup]
G:856 [binder, in mathcomp.fingroup.fingroup]
G:856 [binder, in mathcomp.character.character]
G:857 [binder, in mathcomp.fingroup.fingroup]
G:858 [binder, in mathcomp.character.character]
g:859 [binder, in mathcomp.algebra.vector]
G:86 [binder, in mathcomp.solvable.frobenius]
g:86 [binder, in mathcomp.ssreflect.ssrfun]
G:86 [binder, in mathcomp.solvable.maximal]
G:860 [binder, in mathcomp.fingroup.fingroup]
g:861 [binder, in mathcomp.algebra.vector]
G:861 [binder, in mathcomp.character.character]
G:862 [binder, in mathcomp.character.classfun]
G:862 [binder, in mathcomp.fingroup.fingroup]
G:864 [binder, in mathcomp.character.character]
G:865 [binder, in mathcomp.fingroup.fingroup]
G:866 [binder, in mathcomp.character.classfun]
g:867 [binder, in mathcomp.algebra.matrix]
G:867 [binder, in mathcomp.character.character]
G:868 [binder, in mathcomp.fingroup.fingroup]
g:869 [binder, in mathcomp.algebra.matrix]
G:87 [binder, in mathcomp.solvable.center]
G:87 [binder, in mathcomp.solvable.gfunctor]
G:87 [binder, in mathcomp.fingroup.presentation]
G:870 [binder, in mathcomp.fingroup.fingroup]
G:870 [binder, in mathcomp.character.character]
G:871 [binder, in mathcomp.character.classfun]
G:872 [binder, in mathcomp.fingroup.fingroup]
g:872 [binder, in mathcomp.algebra.vector]
G:872 [binder, in mathcomp.character.character]
G:873 [binder, in mathcomp.character.classfun]
G:874 [binder, in mathcomp.ssreflect.finset]
g:874 [binder, in mathcomp.algebra.matrix]
G:874 [binder, in mathcomp.fingroup.fingroup]
g:874 [binder, in mathcomp.character.mxrepresentation]
G:875 [binder, in mathcomp.fingroup.fingroup]
G:875 [binder, in mathcomp.character.character]
G:876 [binder, in mathcomp.character.classfun]
G:877 [binder, in mathcomp.fingroup.fingroup]
G:878 [binder, in mathcomp.character.character]
G:88 [binder, in mathcomp.solvable.frobenius]
G:88 [binder, in mathcomp.solvable.gseries]
G:880 [binder, in mathcomp.character.classfun]
G:880 [binder, in mathcomp.character.character]
G:883 [binder, in mathcomp.fingroup.fingroup]
G:883 [binder, in mathcomp.character.character]
G:884 [binder, in mathcomp.ssreflect.bigop]
G:885 [binder, in mathcomp.fingroup.fingroup]
G:887 [binder, in mathcomp.fingroup.fingroup]
G:887 [binder, in mathcomp.character.character]
G:889 [binder, in mathcomp.fingroup.fingroup]
G:89 [binder, in mathcomp.solvable.pgroup]
G:89 [binder, in mathcomp.solvable.abelian]
G:89 [binder, in mathcomp.solvable.gfunctor]
G:89 [binder, in mathcomp.solvable.maximal]
G:890 [binder, in mathcomp.ssreflect.finset]
G:890 [binder, in mathcomp.character.character]
G:891 [binder, in mathcomp.fingroup.fingroup]
G:893 [binder, in mathcomp.fingroup.fingroup]
G:894 [binder, in mathcomp.character.classfun]
G:895 [binder, in mathcomp.fingroup.fingroup]
G:897 [binder, in mathcomp.fingroup.fingroup]
G:898 [binder, in mathcomp.character.character]
G:899 [binder, in mathcomp.fingroup.fingroup]
G:9 [binder, in mathcomp.solvable.frobenius]
G:9 [binder, in mathcomp.solvable.gfunctor]
G:9 [binder, in mathcomp.solvable.nilpotent]
G:90 [binder, in mathcomp.fingroup.quotient]
G:90 [binder, in mathcomp.solvable.commutator]
G:90 [binder, in mathcomp.solvable.abelian]
g:90 [binder, in mathcomp.ssreflect.ssrfun]
G:901 [binder, in mathcomp.fingroup.fingroup]
G:903 [binder, in mathcomp.fingroup.fingroup]
g:905 [binder, in mathcomp.algebra.matrix]
G:905 [binder, in mathcomp.fingroup.fingroup]
G:907 [binder, in mathcomp.fingroup.fingroup]
G:909 [binder, in mathcomp.fingroup.fingroup]
G:91 [binder, in mathcomp.solvable.sylow]
G:91 [binder, in mathcomp.solvable.frobenius]
G:91 [binder, in mathcomp.solvable.gfunctor]
G:91 [binder, in mathcomp.solvable.maximal]
G:912 [binder, in mathcomp.character.character]
G:916 [binder, in mathcomp.character.character]
G:918 [binder, in mathcomp.character.character]
G:92 [binder, in mathcomp.fingroup.quotient]
G:92 [binder, in mathcomp.solvable.commutator]
G:92 [binder, in mathcomp.solvable.gseries]
G:92 [binder, in mathcomp.solvable.hall]
G:92 [binder, in mathcomp.fingroup.presentation]
G:92 [binder, in mathcomp.solvable.maximal]
G:920 [binder, in mathcomp.fingroup.fingroup]
G:920 [binder, in mathcomp.character.character]
G:922 [binder, in mathcomp.fingroup.fingroup]
G:922 [binder, in mathcomp.character.character]
G:923 [binder, in mathcomp.fingroup.fingroup]
G:924 [binder, in mathcomp.fingroup.fingroup]
G:926 [binder, in mathcomp.ssreflect.finset]
G:926 [binder, in mathcomp.character.character]
G:928 [binder, in mathcomp.character.character]
G:93 [binder, in mathcomp.fingroup.quotient]
g:93 [binder, in mathcomp.field.separable]
G:93 [binder, in mathcomp.fingroup.gproduct]
G:93 [binder, in mathcomp.solvable.abelian]
G:93 [binder, in mathcomp.solvable.gfunctor]
G:932 [binder, in mathcomp.character.character]
G:94 [binder, in mathcomp.solvable.commutator]
g:94 [binder, in mathcomp.field.separable]
G:94 [binder, in mathcomp.solvable.center]
G:94 [binder, in mathcomp.solvable.maximal]
G:94 [binder, in mathcomp.solvable.nilpotent]
g:946 [binder, in mathcomp.algebra.matrix]
G:95 [binder, in mathcomp.solvable.frobenius]
G:95 [binder, in mathcomp.solvable.abelian]
G:95 [binder, in mathcomp.solvable.hall]
G:95 [binder, in mathcomp.solvable.maximal]
g:952 [binder, in mathcomp.algebra.matrix]
G:96 [binder, in mathcomp.ssreflect.finfun]
G:96 [binder, in mathcomp.solvable.commutator]
G:96 [binder, in mathcomp.solvable.gfunctor]
G:96 [binder, in mathcomp.fingroup.presentation]
G:960 [binder, in mathcomp.fingroup.fingroup]
G:968 [binder, in mathcomp.character.character]
G:97 [binder, in mathcomp.solvable.abelian]
G:972 [binder, in mathcomp.fingroup.fingroup]
G:973 [binder, in mathcomp.fingroup.fingroup]
G:975 [binder, in mathcomp.character.character]
G:976 [binder, in mathcomp.fingroup.fingroup]
G:979 [binder, in mathcomp.fingroup.fingroup]
G:98 [binder, in mathcomp.solvable.pgroup]
g:98 [binder, in mathcomp.ssreflect.order]
G:98 [binder, in mathcomp.solvable.frobenius]
G:98 [binder, in mathcomp.solvable.hall]
g:982 [binder, in mathcomp.ssreflect.finset]
G:986 [binder, in mathcomp.fingroup.fingroup]
G:987 [binder, in mathcomp.fingroup.fingroup]
G:987 [binder, in mathcomp.character.character]
G:988 [binder, in mathcomp.fingroup.fingroup]
g:99 [binder, in mathcomp.character.integral_char]
G:99 [binder, in mathcomp.solvable.commutator]
G:990 [binder, in mathcomp.fingroup.fingroup]
G:995 [binder, in mathcomp.fingroup.fingroup]
g:997 [binder, in mathcomp.character.mxrepresentation]
g:999 [binder, in mathcomp.ssreflect.finset]
G:999 [binder, in mathcomp.fingroup.fingroup]
| 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 | (76754 entries) |
| Notation 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 | (1892 entries) |
| Binder 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 | (49588 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 | (305 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 | (4034 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 | (94 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 | (14802 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 | (222 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 | (9 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 | (131 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 | (43 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 | (1392 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 | (1140 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 | (3066 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 | (36 entries) |