| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -
G
-g [abbreviation, in mathcomp.character.character]-G [abbreviation, in mathcomp.character.inertia]
-G [abbreviation, in mathcomp.character.classfun]
-G [abbreviation, in mathcomp.character.classfun]
-G [abbreviation, in mathcomp.character.classfun]
-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_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]
-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]
-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_is_morphism [lemma, in mathcomp.field.galois]
-gal_finGroupMixin [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_finMixin [definition, in mathcomp.field.galois]
-gal_countMixin [definition, in mathcomp.field.galois]
-gal_choiceMixin [definition, in mathcomp.field.galois]
-gal_eqMixin [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_key [lemma, 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]
-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]
-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]
-generated [definition, in mathcomp.fingroup.fingroup]
-GeneratedGroup [section, in mathcomp.fingroup.fingroup]
-GeneratedGroup.gT [variable, in mathcomp.fingroup.fingroup]
-generatedP [lemma, 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]
-genmx [definition, in mathcomp.algebra.mxalgebra]
-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_key [lemma, in mathcomp.algebra.mxalgebra]
-genmx_def [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_rank [definition, in mathcomp.solvable.abelian]
-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_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_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]
-getCratK [lemma, in mathcomp.field.algC]
-gez0_abs [lemma, in mathcomp.algebra.ssrint]
-ge_rat0_norm [lemma, in mathcomp.algebra.rat]
-ge_rat0 [lemma, in mathcomp.algebra.rat]
-gFchar [lemma, in mathcomp.solvable.gfunctor]
-gFchar_trans [lemma, in mathcomp.solvable.gfunctor]
-gFcompS [lemma, in mathcomp.solvable.gfunctor]
-gFcomp_cont [lemma, in mathcomp.solvable.gfunctor]
-gFcomp_closed [lemma, in mathcomp.solvable.gfunctor]
-gFcont [lemma, 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_hereditary [lemma, in mathcomp.solvable.gfunctor]
-gFmod_cont [lemma, in mathcomp.solvable.gfunctor]
-gFmod_closed [lemma, 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_head [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.IsoMap [constructor, 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 [constructor, 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.MonoMap [constructor, 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]
-GFunctor.Pmap [constructor, in mathcomp.solvable.gfunctor]
-gF1 [lemma, in mathcomp.solvable.gfunctor]
-gH [abbreviation, in mathcomp.fingroup.gproduct]
-gK [abbreviation, in mathcomp.fingroup.gproduct]
-GLgroup [definition, in mathcomp.algebra.matrix]
-GLmx_faithful [lemma, in mathcomp.character.mxabelem]
-GLtype [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_eqMixin [definition, 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]
-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 [definition, in mathcomp.character.integral_char]
-gring_irr_mode_def [definition, in mathcomp.character.integral_char]
-gring_irr_mode_key [lemma, 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.add [definition, in mathcomp.algebra.ssralg]
-GRing.addf_div [lemma, in mathcomp.algebra.ssralg]
-GRing.addIr [lemma, in mathcomp.algebra.ssralg]
-GRing.Additive [module, in mathcomp.algebra.ssralg]
-GRing.AdditiveTheory [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.g [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.V [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.f [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.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.Additive.apply [projection, in mathcomp.algebra.ssralg]
-GRing.Additive.axiom [definition, in mathcomp.algebra.ssralg]
-GRing.Additive.class [definition, in mathcomp.algebra.ssralg]
-GRing.Additive.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.Additive.ClassDef.cF [variable, in mathcomp.algebra.ssralg]
-GRing.Additive.ClassDef.f [variable, in mathcomp.algebra.ssralg]
-GRing.Additive.ClassDef.g [variable, in mathcomp.algebra.ssralg]
-GRing.Additive.ClassDef.phUV [variable, in mathcomp.algebra.ssralg]
-GRing.Additive.ClassDef.U [variable, in mathcomp.algebra.ssralg]
-GRing.Additive.ClassDef.V [variable, in mathcomp.algebra.ssralg]
-GRing.Additive.clone [definition, in mathcomp.algebra.ssralg]
-GRing.Additive.Exports [module, in mathcomp.algebra.ssralg]
-GRing.Additive.Exports.Additive [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Additive.Exports.additive [abbreviation, in mathcomp.algebra.ssralg]
-[ additive of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ additive of _ as _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-{ additive _ } (ring_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.Additive.map [record, in mathcomp.algebra.ssralg]
-GRing.Additive.Pack [constructor, 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.addNr [lemma, in mathcomp.algebra.ssralg]
-GRing.addrA [lemma, in mathcomp.algebra.ssralg]
-GRing.addrAC [lemma, in mathcomp.algebra.ssralg]
-GRing.addrACA [lemma, in mathcomp.algebra.ssralg]
-GRing.addrC [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_closed [definition, in mathcomp.algebra.ssralg]
-GRing.addr_eq0 [lemma, 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_additive [lemma, in mathcomp.algebra.ssralg]
-GRing.add_fun_head [definition, in mathcomp.algebra.ssralg]
-GRing.add0r [lemma, in mathcomp.algebra.ssralg]
-GRing.Algebra [module, 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.U [variable, in mathcomp.algebra.ssralg]
-GRing.Algebra.axiom [definition, in mathcomp.algebra.ssralg]
-GRing.Algebra.base [projection, in mathcomp.algebra.ssralg]
-GRing.Algebra.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.Algebra.class [definition, in mathcomp.algebra.ssralg]
-GRing.Algebra.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.Algebra.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.Algebra.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.Algebra.ClassDef.phR [variable, in mathcomp.algebra.ssralg]
-GRing.Algebra.ClassDef.R [variable, in mathcomp.algebra.ssralg]
-GRing.Algebra.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.Algebra.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.Algebra.class_of [record, in mathcomp.algebra.ssralg]
-GRing.Algebra.clone [definition, in mathcomp.algebra.ssralg]
-GRing.Algebra.comm_axiom [lemma, in mathcomp.algebra.ssralg]
-GRing.Algebra.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.Algebra.Exports [module, in mathcomp.algebra.ssralg]
-GRing.Algebra.Exports.AlgType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Algebra.Exports.algType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Algebra.Exports.CommAlgType [abbreviation, in mathcomp.algebra.ssralg]
-[ algType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ algType _ of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.Algebra.lalgType [definition, in mathcomp.algebra.ssralg]
-GRing.Algebra.lmodType [definition, in mathcomp.algebra.ssralg]
-GRing.Algebra.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.Algebra.Mixin [section, in mathcomp.algebra.ssralg]
-GRing.Algebra.Mixin.A [variable, in mathcomp.algebra.ssralg]
-GRing.Algebra.Mixin.R [variable, in mathcomp.algebra.ssralg]
-GRing.Algebra.pack [definition, in mathcomp.algebra.ssralg]
-GRing.Algebra.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.Algebra.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.Algebra.sort [projection, in mathcomp.algebra.ssralg]
-GRing.Algebra.type [record, in mathcomp.algebra.ssralg]
-GRing.Algebra.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Algebra.zmodType [definition, 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.bij_lrmorphism [lemma, in mathcomp.algebra.ssralg]
-GRing.bij_linear [lemma, in mathcomp.algebra.ssralg]
-GRing.bij_rmorphism [lemma, in mathcomp.algebra.ssralg]
-GRing.bij_additive [lemma, in mathcomp.algebra.ssralg]
-GRing.bin_lt_charf_0 [lemma, in mathcomp.algebra.ssralg]
-GRing.Bool [constructor, in mathcomp.algebra.ssralg]
-GRing.can2_lrmorphism [lemma, in mathcomp.algebra.ssralg]
-GRing.can2_linear [lemma, in mathcomp.algebra.ssralg]
-GRing.can2_rmorphism [lemma, in mathcomp.algebra.ssralg]
-GRing.can2_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.ClosedField [module, in mathcomp.algebra.ssralg]
-GRing.ClosedFieldTheory [section, in mathcomp.algebra.ssralg]
-GRing.ClosedFieldTheory.F [variable, in mathcomp.algebra.ssralg]
-GRing.ClosedField.axiom [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.base [projection, in mathcomp.algebra.ssralg]
-GRing.ClosedField.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.class [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.ClosedField.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.ClosedField.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.ClosedField.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.ClosedField.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.ClosedField.class_of [record, in mathcomp.algebra.ssralg]
-GRing.ClosedField.clone [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.comRingType [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.comUnitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.decFieldType [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.Exports [module, in mathcomp.algebra.ssralg]
-GRing.ClosedField.Exports.ClosedFieldType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.ClosedField.Exports.closedFieldType [abbreviation, in mathcomp.algebra.ssralg]
-[ closedFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ closedFieldType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.ClosedField.fieldType [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.idomainType [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.pack [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.ClosedField.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.sort [projection, in mathcomp.algebra.ssralg]
-GRing.ClosedField.type [record, in mathcomp.algebra.ssralg]
-GRing.ClosedField.unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.ClosedField.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.ClosedField.zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.comm [definition, 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_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.comp_lrmorphism [definition, 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_additive [lemma, in mathcomp.algebra.ssralg]
-GRing.ComRing [module, 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.ComRing.base [projection, in mathcomp.algebra.ssralg]
-GRing.ComRing.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.ComRing.class [definition, in mathcomp.algebra.ssralg]
-GRing.ComRing.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.ComRing.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.ComRing.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.ComRing.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.ComRing.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.ComRing.class_of [record, in mathcomp.algebra.ssralg]
-GRing.ComRing.clone [definition, in mathcomp.algebra.ssralg]
-GRing.ComRing.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.ComRing.Exports [module, in mathcomp.algebra.ssralg]
-GRing.ComRing.Exports.ComRingMixin [abbreviation, in mathcomp.algebra.ssralg]
-GRing.ComRing.Exports.ComRingType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.ComRing.Exports.comRingType [abbreviation, in mathcomp.algebra.ssralg]
-[ comRingType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ comRingType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.ComRing.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.ComRing.pack [definition, in mathcomp.algebra.ssralg]
-GRing.ComRing.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.ComRing.RingMixin [definition, in mathcomp.algebra.ssralg]
-GRing.ComRing.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.ComRing.sort [projection, in mathcomp.algebra.ssralg]
-GRing.ComRing.type [record, in mathcomp.algebra.ssralg]
-GRing.ComRing.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.ComRing.zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing [module, in mathcomp.algebra.ssralg]
-GRing.ComUnitRingTheory [section, in mathcomp.algebra.ssralg]
-GRing.ComUnitRingTheory.R [variable, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.base [projection, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.base2 [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.class [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.class_of [record, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.comRingType [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.com_unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Exports [module, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Exports.ComUnitRingMixin [abbreviation, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Exports.comUnitRingType [abbreviation, in mathcomp.algebra.ssralg]
-[ comUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Mixin [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Mixin [section, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Mixin.inv [variable, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Mixin.mulVx [variable, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Mixin.R [variable, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Mixin.unit [variable, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Mixin.unitPl [variable, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.mulC_unitP [lemma, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.mulC_mulrV [lemma, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.pack [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.sort [projection, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.type [record, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.ComUnitRing.zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.Const [constructor, in mathcomp.algebra.ssralg]
-GRing.converse [definition, in mathcomp.algebra.ssralg]
-GRing.converse_unitRingMixin [definition, in mathcomp.algebra.ssralg]
-GRing.converse_ringMixin [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField [module, in mathcomp.algebra.ssralg]
-GRing.DecidableFieldTheory [section, in mathcomp.algebra.ssralg]
-GRing.DecidableFieldTheory.F [variable, in mathcomp.algebra.ssralg]
-GRing.DecidableField.axiom [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.base [projection, in mathcomp.algebra.ssralg]
-GRing.DecidableField.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.class [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.DecidableField.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.DecidableField.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.DecidableField.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.DecidableField.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.DecidableField.class_of [record, in mathcomp.algebra.ssralg]
-GRing.DecidableField.clone [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.comRingType [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.comUnitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.Exports [module, in mathcomp.algebra.ssralg]
-GRing.DecidableField.Exports.DecFieldMixin [abbreviation, in mathcomp.algebra.ssralg]
-GRing.DecidableField.Exports.DecFieldType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.DecidableField.Exports.decFieldType [abbreviation, in mathcomp.algebra.ssralg]
-[ decFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ decFieldType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.DecidableField.fieldType [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.idomainType [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.DecidableField.Mixin [constructor, in mathcomp.algebra.ssralg]
-GRing.DecidableField.mixin_of [record, in mathcomp.algebra.ssralg]
-GRing.DecidableField.pack [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.DecidableField.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.sat [projection, in mathcomp.algebra.ssralg]
-GRing.DecidableField.satP [projection, in mathcomp.algebra.ssralg]
-GRing.DecidableField.sort [projection, in mathcomp.algebra.ssralg]
-GRing.DecidableField.type [record, in mathcomp.algebra.ssralg]
-GRing.DecidableField.unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.DecidableField.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.DecidableField.zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.DefaultPred [module, 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.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.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_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.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.Field [module, in mathcomp.algebra.ssralg]
-GRing.fieldP [lemma, 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.FieldTheory.Predicates [section, in mathcomp.algebra.ssralg]
-GRing.Field.axiom [definition, in mathcomp.algebra.ssralg]
-GRing.Field.base [projection, in mathcomp.algebra.ssralg]
-GRing.Field.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.Field.class [definition, in mathcomp.algebra.ssralg]
-GRing.Field.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.Field.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.Field.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.Field.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.Field.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.Field.class_of [record, in mathcomp.algebra.ssralg]
-GRing.Field.clone [definition, in mathcomp.algebra.ssralg]
-GRing.Field.comRingType [definition, in mathcomp.algebra.ssralg]
-GRing.Field.comUnitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.Field.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.Field.Exports [module, in mathcomp.algebra.ssralg]
-GRing.Field.Exports.FieldIdomainMixin [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Field.Exports.FieldMixin [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Field.Exports.FieldType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Field.Exports.fieldType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Field.Exports.FieldUnitMixin [abbreviation, in mathcomp.algebra.ssralg]
-[ fieldType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ fieldType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.Field.IdomainMixin [lemma, in mathcomp.algebra.ssralg]
-GRing.Field.idomainType [definition, in mathcomp.algebra.ssralg]
-GRing.Field.IdomainType [definition, in mathcomp.algebra.ssralg]
-GRing.Field.intro_unit [lemma, in mathcomp.algebra.ssralg]
-GRing.Field.inv_out [lemma, in mathcomp.algebra.ssralg]
-GRing.Field.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.Field.Mixin [lemma, in mathcomp.algebra.ssralg]
-GRing.Field.Mixins [section, in mathcomp.algebra.ssralg]
-GRing.Field.Mixins.inv [variable, in mathcomp.algebra.ssralg]
-GRing.Field.Mixins.inv0 [variable, in mathcomp.algebra.ssralg]
-GRing.Field.Mixins.mulVf [variable, in mathcomp.algebra.ssralg]
-GRing.Field.Mixins.R [variable, in mathcomp.algebra.ssralg]
-GRing.Field.mixin_of [definition, in mathcomp.algebra.ssralg]
-GRing.Field.pack [definition, in mathcomp.algebra.ssralg]
-GRing.Field.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.Field.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.Field.sort [projection, in mathcomp.algebra.ssralg]
-GRing.Field.type [record, in mathcomp.algebra.ssralg]
-GRing.Field.UnitMixin [definition, in mathcomp.algebra.ssralg]
-GRing.Field.unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.Field.UnitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.Field.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Field.zmodType [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_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_rmorphism [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_lrmorphism [definition, 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_additive [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.IntegralDomain [module, in mathcomp.algebra.ssralg]
-GRing.IntegralDomainTheory [section, in mathcomp.algebra.ssralg]
-GRing.IntegralDomainTheory.R [variable, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.axiom [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.base [projection, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.class [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.class_of [record, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.clone [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.comRingType [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.comUnitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.Exports [module, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.Exports.IdomainType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.Exports.idomainType [abbreviation, in mathcomp.algebra.ssralg]
-[ idomainType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ idomainType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.pack [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.sort [projection, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.type [record, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.IntegralDomain.zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.Inv [constructor, in mathcomp.algebra.ssralg]
-GRing.inv [definition, 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_loc [abbreviation, in mathcomp.algebra.ssralg]
-GRing.in_alg_head [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra [module, 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.Lalgebra.axiom [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.base [projection, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.base2 [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.class [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.ClassDef.phR [variable, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.ClassDef.R [variable, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.class_of [record, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.clone [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.Exports [module, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.Exports.LalgType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.Exports.lalgType [abbreviation, in mathcomp.algebra.ssralg]
-[ lalgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ lalgType _ of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.ext [projection, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.lmodType [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.lmod_ringType [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.pack [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.sort [projection, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.type [record, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Lalgebra.zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.lastr_eq0 [lemma, in mathcomp.algebra.ssralg]
-GRing.LiftedRing [section, in mathcomp.algebra.ssralg]
-GRing.LiftedRing.R [variable, in mathcomp.algebra.ssralg]
-GRing.LiftedRing.T [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.LiftedZmod [section, in mathcomp.algebra.ssralg]
-GRing.LiftedZmod.U [variable, in mathcomp.algebra.ssralg]
-GRing.LiftedZmod.V [variable, in mathcomp.algebra.ssralg]
-GRing.Linear [module, in mathcomp.algebra.ssralg]
-GRing.linearB [lemma, in mathcomp.algebra.ssralg]
-GRing.linearD [lemma, 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.h_law [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.Ds [variable, in mathcomp.algebra.ssralg]
-GRing.LinearTheory.LinearLmod.f [variable, in mathcomp.algebra.ssralg]
-GRing.LinearTheory.LinearLmod.g [variable, in mathcomp.algebra.ssralg]
-GRing.LinearTheory.LinearLmod.h [variable, in mathcomp.algebra.ssralg]
-GRing.LinearTheory.LinearLmod.s [variable, in mathcomp.algebra.ssralg]
-GRing.LinearTheory.LinearLmod.s_law [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_closedB [lemma, in mathcomp.algebra.ssralg]
-GRing.linear_closed [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.apply [projection, in mathcomp.algebra.ssralg]
-GRing.Linear.axiom [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.base [projection, in mathcomp.algebra.ssralg]
-GRing.Linear.class [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.Linear.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.Linear.ClassDef.cF [variable, in mathcomp.algebra.ssralg]
-GRing.Linear.ClassDef.f [variable, in mathcomp.algebra.ssralg]
-GRing.Linear.ClassDef.g [variable, in mathcomp.algebra.ssralg]
-GRing.Linear.ClassDef.phUV [variable, in mathcomp.algebra.ssralg]
-GRing.Linear.ClassDef.R [variable, in mathcomp.algebra.ssralg]
-GRing.Linear.ClassDef.s [variable, in mathcomp.algebra.ssralg]
-GRing.Linear.ClassDef.U [variable, in mathcomp.algebra.ssralg]
-GRing.Linear.ClassDef.V [variable, in mathcomp.algebra.ssralg]
-GRing.Linear.class_of_axiom [lemma, in mathcomp.algebra.ssralg]
-GRing.Linear.class_of [record, in mathcomp.algebra.ssralg]
-GRing.Linear.clone [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports [module, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports.AddLinear [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports.Linear [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports.linear [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports.linear_for [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports.lmorphism [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports.lmorphism_for [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports.scalable [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports.scalable_for [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Linear.Exports.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]
-_ *^ _ _ (linear_ring_scope) [notation, in mathcomp.algebra.ssralg]
-_ *:^ _ _ (linear_ring_scope) [notation, in mathcomp.algebra.ssralg]
-_ * _ (linear_ring_scope) [notation, in mathcomp.algebra.ssralg]
-_ *: _ (linear_ring_scope) [notation, in mathcomp.algebra.ssralg]
-{ scalar _ } (ring_scope) [notation, in mathcomp.algebra.ssralg]
-{ linear _ } (ring_scope) [notation, in mathcomp.algebra.ssralg]
-{ linear _ | _ } (ring_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.Linear.map [record, in mathcomp.algebra.ssralg]
-GRing.Linear.MapFor [constructor, in mathcomp.algebra.ssralg]
-GRing.Linear.mapUV [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Linear.map_for_map [projection, in mathcomp.algebra.ssralg]
-GRing.Linear.map_for [record, in mathcomp.algebra.ssralg]
-GRing.Linear.map_at [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.map_class [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.Linear.mixin_of [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.pack [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.Linear.unify_map_at [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.unwrap [projection, in mathcomp.algebra.ssralg]
-GRing.Linear.wrap [definition, in mathcomp.algebra.ssralg]
-GRing.Linear.Wrap [constructor, in mathcomp.algebra.ssralg]
-GRing.Linear.wrapped [record, in mathcomp.algebra.ssralg]
-GRing.linear0 [lemma, in mathcomp.algebra.ssralg]
-GRing.LmodPred [section, in mathcomp.algebra.ssralg]
-GRing.LmodPred.R [variable, in mathcomp.algebra.ssralg]
-GRing.LmodPred.S [variable, in mathcomp.algebra.ssralg]
-GRing.LmodPred.V [variable, in mathcomp.algebra.ssralg]
-GRing.Lmodule [module, 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]
-*:%R [notation, in mathcomp.algebra.ssralg]
-GRing.Lmodule.base [projection, in mathcomp.algebra.ssralg]
-GRing.Lmodule.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.Lmodule.class [definition, in mathcomp.algebra.ssralg]
-GRing.Lmodule.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.Lmodule.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.Lmodule.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.Lmodule.ClassDef.phR [variable, in mathcomp.algebra.ssralg]
-GRing.Lmodule.ClassDef.R [variable, in mathcomp.algebra.ssralg]
-GRing.Lmodule.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.Lmodule.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.Lmodule.class_of [record, in mathcomp.algebra.ssralg]
-GRing.Lmodule.clone [definition, in mathcomp.algebra.ssralg]
-GRing.Lmodule.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.Lmodule.Exports [module, in mathcomp.algebra.ssralg]
-GRing.Lmodule.Exports.LmodMixin [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Lmodule.Exports.LmodType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Lmodule.Exports.lmodType [abbreviation, in mathcomp.algebra.ssralg]
-[ lmodType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ lmodType _ of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.Lmodule.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.Lmodule.Mixin [constructor, in mathcomp.algebra.ssralg]
-GRing.Lmodule.mixin_of [record, in mathcomp.algebra.ssralg]
-GRing.Lmodule.pack [definition, in mathcomp.algebra.ssralg]
-GRing.Lmodule.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.Lmodule.scale [projection, in mathcomp.algebra.ssralg]
-GRing.Lmodule.sort [projection, in mathcomp.algebra.ssralg]
-GRing.Lmodule.type [record, in mathcomp.algebra.ssralg]
-GRing.Lmodule.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Lmodule.zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.locked_lrmorphism [definition, in mathcomp.algebra.ssralg]
-GRing.locked_is_scalable [lemma, in mathcomp.algebra.ssralg]
-GRing.locked_is_multiplicative [lemma, in mathcomp.algebra.ssralg]
-GRing.locked_is_additive [lemma, in mathcomp.algebra.ssralg]
-GRing.lreg [definition, in mathcomp.algebra.ssralg]
-GRing.lregM [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.LRMorphism [module, in mathcomp.algebra.ssralg]
-GRing.lrmorphismP [lemma, 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.LRMorphism.apply [projection, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.base [projection, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.base2 [definition, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.class [definition, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.ClassDef.A [variable, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.ClassDef.B [variable, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.ClassDef.cF [variable, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.ClassDef.f [variable, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.ClassDef.phAB [variable, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.ClassDef.R [variable, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.ClassDef.s [variable, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.class_of [record, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.clone [definition, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.Exports [module, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.Exports.AddLRMorphism [abbreviation, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.Exports.LRMorphism [abbreviation, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.Exports.lrmorphism [abbreviation, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.Exports.lrmorphism_for [abbreviation, in mathcomp.algebra.ssralg]
-[ lrmorphism of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-{ lrmorphism _ } (ring_scope) [notation, in mathcomp.algebra.ssralg]
-{ lrmorphism _ | _ } (ring_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.map [record, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.pack [definition, in mathcomp.algebra.ssralg]
-GRing.LRMorphism.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.Mul [constructor, in mathcomp.algebra.ssralg]
-GRing.mul [definition, 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_additive [lemma, in mathcomp.algebra.ssralg]
-GRing.mull_fun_head [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.mulrA [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.mulrC [lemma, in mathcomp.algebra.ssralg]
-GRing.mulrCA [lemma, in mathcomp.algebra.ssralg]
-GRing.mulrDl [lemma, in mathcomp.algebra.ssralg]
-GRing.mulrDr [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_additive [lemma, in mathcomp.algebra.ssralg]
-GRing.mulr_fun_head [definition, in mathcomp.algebra.ssralg]
-GRing.mulr_algl [lemma, in mathcomp.algebra.ssralg]
-GRing.mulr_closed [definition, in mathcomp.algebra.ssralg]
-GRing.mulr_2closed [definition, in mathcomp.algebra.ssralg]
-GRing.mulr_signM [lemma, in mathcomp.algebra.ssralg]
-GRing.mulr_sign [lemma, 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.mulr0 [lemma, in mathcomp.algebra.ssralg]
-GRing.mulr0n [lemma, in mathcomp.algebra.ssralg]
-GRing.mulr1 [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.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.mul0r [lemma, in mathcomp.algebra.ssralg]
-GRing.mul0rn [lemma, in mathcomp.algebra.ssralg]
-GRing.mul1r [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.Not [constructor, in mathcomp.algebra.ssralg]
-GRing.null_fun_is_scalable [lemma, in mathcomp.algebra.ssralg]
-GRing.null_fun_is_additive [lemma, in mathcomp.algebra.ssralg]
-GRing.null_fun [abbreviation, in mathcomp.algebra.ssralg]
-GRing.null_fun_head [definition, in mathcomp.algebra.ssralg]
-GRing.one [definition, in mathcomp.algebra.ssralg]
-GRing.oner_eq0 [lemma, in mathcomp.algebra.ssralg]
-GRing.oner_neq0 [lemma, in mathcomp.algebra.ssralg]
-GRing.Opp [constructor, in mathcomp.algebra.ssralg]
-GRing.opp [definition, 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_is_scalable [lemma, in mathcomp.algebra.ssralg]
-GRing.opp_is_additive [lemma, 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.Pred [module, in mathcomp.algebra.ssralg]
-GRing.Pred.add [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Add [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.add_ext [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.add_key [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.Default [module, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.add [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.div [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.divalg [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.divring [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.mul [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.opp [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.sdiv [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.semiring [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.smul [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.subalg [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.submod [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.subring [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Default.zmod [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.div [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Div [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.divalg [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Divalg [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.divalg_alg [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.divalg_scaler [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.divalg_ring [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.divring [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Divring [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.divring_sdiv [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.divring_invr [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.divring_ring [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.div_mul [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports [module, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.AddrPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.addrPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.addr_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.DivalgPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.divalgPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.divalg_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.DivringPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.divringPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.divring_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.DivrPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.divrPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.divr_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.invr_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.linear_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.MulrPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.mulrPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.mulr_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.OpprPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.opprPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.oppr_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.scaler_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.SdivrPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.sdivrPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.sdivr_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.SemiringPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.semiringPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.semiring_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.SmulrPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.smulrPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.smulr_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.SubalgPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.subalgPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.subalg_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.SubmodPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.submodPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.submod_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.SubringPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.subringPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.subring_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.ZmodPred [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.zmodPred [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Exports.zmod_closed [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Pred.Extensionality [section, in mathcomp.algebra.ssralg]
-GRing.Pred.inv_ext [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.mul [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Mul [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.mul_ext [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.mul_key [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.opp [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Opp [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.opp_ext [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.opp_key [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.scale_ext [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.sdiv [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Sdiv [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.sdiv_div [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.sdiv_invr [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.sdiv_smul [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.semiring [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Semiring [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.semiring_mul [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.semiring_mulr [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.semiring_add [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.smul [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Smul [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.smul_mul [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.smul_mulr [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.smul_opp [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.subalg [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Subalg [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.subalg_submod [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.subalg_scaler [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.subalg_ring [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.submod [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Submod [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.submod_scaler [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.submod_zmod [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.subring [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Subring [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.subring_smul [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.subring_semi [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.subring_mulr [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.subring_zmod [projection, in mathcomp.algebra.ssralg]
-GRing.Pred.Subtyping [section, in mathcomp.algebra.ssralg]
-GRing.Pred.zmod [record, in mathcomp.algebra.ssralg]
-GRing.Pred.Zmod [constructor, in mathcomp.algebra.ssralg]
-GRing.Pred.zmod_opp [definition, in mathcomp.algebra.ssralg]
-GRing.Pred.zmod_oppr [lemma, in mathcomp.algebra.ssralg]
-GRing.Pred.zmod_add [projection, 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.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 [lemma, in mathcomp.algebra.ssralg]
-GRing.proj_satP [lemma, in mathcomp.algebra.ssralg]
-GRing.proj_sat [definition, in mathcomp.algebra.ssralg]
-GRing.QEdecFieldMixin [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_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.regular_lmodMixin [definition, 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.RightRegular.Rc [variable, in mathcomp.algebra.ssralg]
-GRing.Ring [module, in mathcomp.algebra.ssralg]
-GRing.RingPred [section, in mathcomp.algebra.ssralg]
-GRing.RingPred.Mul [section, in mathcomp.algebra.ssralg]
-GRing.RingPred.Mul.kS [variable, in mathcomp.algebra.ssralg]
-GRing.RingPred.Mul.mulS [variable, in mathcomp.algebra.ssralg]
-GRing.RingPred.R [variable, in mathcomp.algebra.ssralg]
-GRing.RingPred.S [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.Ring.base [projection, in mathcomp.algebra.ssralg]
-GRing.Ring.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.Ring.class [definition, in mathcomp.algebra.ssralg]
-GRing.Ring.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.Ring.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.Ring.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.Ring.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.Ring.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.Ring.class_of [record, in mathcomp.algebra.ssralg]
-GRing.Ring.clone [definition, in mathcomp.algebra.ssralg]
-GRing.Ring.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.Ring.EtaMixin [definition, in mathcomp.algebra.ssralg]
-GRing.Ring.Exports [module, in mathcomp.algebra.ssralg]
-GRing.Ring.Exports.RingMixin [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Ring.Exports.RingType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Ring.Exports.ringType [abbreviation, in mathcomp.algebra.ssralg]
-[ ringType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ ringType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.Ring.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.Ring.Mixin [constructor, in mathcomp.algebra.ssralg]
-GRing.Ring.mixin_of [record, in mathcomp.algebra.ssralg]
-GRing.Ring.mul [projection, in mathcomp.algebra.ssralg]
-GRing.Ring.one [projection, in mathcomp.algebra.ssralg]
-GRing.Ring.pack [definition, in mathcomp.algebra.ssralg]
-GRing.Ring.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.Ring.sort [projection, in mathcomp.algebra.ssralg]
-GRing.Ring.type [record, in mathcomp.algebra.ssralg]
-GRing.Ring.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Ring.zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.rmorphB [lemma, in mathcomp.algebra.ssralg]
-GRing.rmorphD [lemma, in mathcomp.algebra.ssralg]
-GRing.RMorphism [module, in mathcomp.algebra.ssralg]
-GRing.rmorphismMP [lemma, in mathcomp.algebra.ssralg]
-GRing.rmorphismP [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.f [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.S [variable, in mathcomp.algebra.ssralg]
-GRing.RMorphism.apply [projection, in mathcomp.algebra.ssralg]
-GRing.RMorphism.base [projection, in mathcomp.algebra.ssralg]
-GRing.RMorphism.class [definition, in mathcomp.algebra.ssralg]
-GRing.RMorphism.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.RMorphism.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.RMorphism.ClassDef.cF [variable, in mathcomp.algebra.ssralg]
-GRing.RMorphism.ClassDef.f [variable, in mathcomp.algebra.ssralg]
-GRing.RMorphism.ClassDef.g [variable, in mathcomp.algebra.ssralg]
-GRing.RMorphism.ClassDef.phRS [variable, in mathcomp.algebra.ssralg]
-GRing.RMorphism.ClassDef.R [variable, in mathcomp.algebra.ssralg]
-GRing.RMorphism.ClassDef.S [variable, in mathcomp.algebra.ssralg]
-GRing.RMorphism.class_of [record, in mathcomp.algebra.ssralg]
-GRing.RMorphism.clone [definition, in mathcomp.algebra.ssralg]
-GRing.RMorphism.Exports [module, in mathcomp.algebra.ssralg]
-GRing.RMorphism.Exports.AddRMorphism [abbreviation, in mathcomp.algebra.ssralg]
-GRing.RMorphism.Exports.multiplicative [abbreviation, in mathcomp.algebra.ssralg]
-GRing.RMorphism.Exports.RMorphism [abbreviation, in mathcomp.algebra.ssralg]
-GRing.RMorphism.Exports.rmorphism [abbreviation, in mathcomp.algebra.ssralg]
-[ rmorphism of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ rmorphism of _ as _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-{ rmorphism _ } (ring_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.RMorphism.map [record, in mathcomp.algebra.ssralg]
-GRing.RMorphism.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.RMorphism.mixin_of [definition, in mathcomp.algebra.ssralg]
-GRing.RMorphism.pack [definition, in mathcomp.algebra.ssralg]
-GRing.RMorphism.Pack [constructor, 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.rmorphX [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_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_sign [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.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.rpredM [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.rpredNr [lemma, in mathcomp.algebra.ssralg]
-GRing.rpredN1 [lemma, in mathcomp.algebra.ssralg]
-GRing.rpredV [lemma, in mathcomp.algebra.ssralg]
-GRing.rpredVr [lemma, in mathcomp.algebra.ssralg]
-GRing.rpredX [lemma, in mathcomp.algebra.ssralg]
-GRing.rpredXN [lemma, in mathcomp.algebra.ssralg]
-GRing.rpredZ [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.rpred0D [lemma, in mathcomp.algebra.ssralg]
-GRing.rpred1 [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.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.sat [definition, in mathcomp.algebra.ssralg]
-GRing.satP [lemma, 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.scale [definition, in mathcomp.algebra.ssralg]
-GRing.scaleNr [lemma, in mathcomp.algebra.ssralg]
-GRing.scaleN1r [lemma, in mathcomp.algebra.ssralg]
-GRing.scalerA [lemma, in mathcomp.algebra.ssralg]
-GRing.scalerAl [lemma, in mathcomp.algebra.ssralg]
-GRing.scalerAr [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.scalerDl [lemma, in mathcomp.algebra.ssralg]
-GRing.scalerDr [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_head [definition, in mathcomp.algebra.ssralg]
-GRing.Scale.compN1op [lemma, in mathcomp.algebra.ssralg]
-GRing.Scale.comp_law [definition, in mathcomp.algebra.ssralg]
-GRing.Scale.comp_opE [lemma, in mathcomp.algebra.ssralg]
-GRing.Scale.law [record, in mathcomp.algebra.ssralg]
-GRing.Scale.Law [constructor, in mathcomp.algebra.ssralg]
-GRing.Scale.mul_law [definition, in mathcomp.algebra.ssralg]
-GRing.Scale.N1op [lemma, in mathcomp.algebra.ssralg]
-GRing.Scale.op [projection, in mathcomp.algebra.ssralg]
-GRing.Scale.opB [lemma, in mathcomp.algebra.ssralg]
-GRing.Scale.opE [lemma, in mathcomp.algebra.ssralg]
-GRing.Scale.op_additive [definition, 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 [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.Scale.scale_law [definition, in mathcomp.algebra.ssralg]
-GRing.Scale.s_op [abbreviation, in mathcomp.algebra.ssralg]
-GRing.scale0r [lemma, in mathcomp.algebra.ssralg]
-GRing.scale1r [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.semiring_closedM [lemma, in mathcomp.algebra.ssralg]
-GRing.semiring_closedD [lemma, in mathcomp.algebra.ssralg]
-GRing.semiring_closed [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.solve_monicpoly [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.subalg_closedBM [lemma, in mathcomp.algebra.ssralg]
-GRing.subalg_closedZ [lemma, in mathcomp.algebra.ssralg]
-GRing.subalg_closed [definition, in mathcomp.algebra.ssralg]
-GRing.subIr [lemma, in mathcomp.algebra.ssralg]
-GRing.subKr [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.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.SubType [module, in mathcomp.algebra.ssralg]
-GRing.SubType.addA [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.addC [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.addN [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.add0 [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.algMixin [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.cast_ringType [definition, in mathcomp.algebra.ssralg]
-GRing.SubType.cast_zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.SubType.comRingMixin [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.Exports [module, in mathcomp.algebra.ssralg]
-[ fieldMixin of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ idomainMixin of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ unitRingMixin of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ algMixin of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ comRingMixin of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ lalgMixin of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ lmodMixin of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ ringMixin of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ zmodMixin of _ by <: ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.SubType.fieldMixin [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.idomainMixin [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.lalgMixin [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.lmodMixin [definition, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule [section, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.kS [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.linS [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.R [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.S [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.scaleW [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.V [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.valD [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.W [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.W' [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.Z [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Lmodule.ZeqW [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.mulA [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.mulDl [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.mulDr [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.mulrV [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.mulVr [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.mul1l [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.mul1r [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.nz1 [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring [section, in mathcomp.algebra.ssralg]
-GRing.SubType.ringMixin [definition, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.inT [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.kS [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.mulT [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.oneT [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.R [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.ringS [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.S [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.T [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.T' [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.V [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.valD [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.valM [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.val0 [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Ring.VeqT [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.scaleA [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.scaleDl [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.scaleDr [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.scale1 [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.unitP [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing [section, in mathcomp.algebra.ssralg]
-GRing.SubType.unitRingMixin [definition, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.inT [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.invT [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.kS [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.Q [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.QeqT [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.R [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.ringS [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.S [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.T [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.T' [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.unitT [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.valM [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.UnitRing.val1 [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.unit_id [lemma, in mathcomp.algebra.ssralg]
-GRing.SubType.zmodMixin [definition, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule [section, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule.addU [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule.inU [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule.kS [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule.oppU [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule.S [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule.subS [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule.U [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule.V [variable, in mathcomp.algebra.ssralg]
-GRing.SubType.Zmodule.zeroU [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_head [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 [lemma, in mathcomp.algebra.ssralg]
-GRing.telescope_prodf [lemma, in mathcomp.algebra.ssralg]
-GRing.telescope_prodr [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.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.bij_lrmorphism [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.bij_linear [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.bij_rmorphism [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.bij_additive [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.bin_lt_charf_0 [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.can2_lrmorphism [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.can2_linear [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.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.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_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.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.divrK [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_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.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_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.linearB [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.linearD [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.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.lrmorphismP [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.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.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.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 [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_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.rmorphismMP [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.rmorphismP [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 [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.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.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.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.subIr [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.subKr [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.subrI [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 [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.telescope_prodf [definition, in mathcomp.algebra.ssralg]
-GRing.Theory.telescope_prodr [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.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.UnitAlgebra [module, 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.UnitAlgebra.algType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.alg_unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.base [projection, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.base2 [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.class [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.ClassDef.phR [variable, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.ClassDef.R [variable, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.class_of [record, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.Exports [module, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.Exports.unitAlgType [abbreviation, in mathcomp.algebra.ssralg]
-[ unitAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.lalgType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.lalg_unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.lmodType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.lmod_unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.pack [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.sort [projection, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.type [record, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.unitRingType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.UnitAlgebra.zmodType [definition, in mathcomp.algebra.ssralg]
-GRing.unitfE [lemma, in mathcomp.algebra.ssralg]
-GRing.unitrE [lemma, in mathcomp.algebra.ssralg]
-GRing.UnitRing [module, 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.divS [variable, in mathcomp.algebra.ssralg]
-GRing.UnitRingPred.Div.kS [variable, 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.ClosedPredicates [section, in mathcomp.algebra.ssralg]
-GRing.UnitRingTheory.ClosedPredicates.S [variable, in mathcomp.algebra.ssralg]
-GRing.UnitRingTheory.R [variable, in mathcomp.algebra.ssralg]
-GRing.UnitRing.base [projection, in mathcomp.algebra.ssralg]
-GRing.UnitRing.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitRing.class [definition, in mathcomp.algebra.ssralg]
-GRing.UnitRing.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.UnitRing.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.UnitRing.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.UnitRing.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.UnitRing.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.UnitRing.class_of [record, in mathcomp.algebra.ssralg]
-GRing.UnitRing.clone [definition, in mathcomp.algebra.ssralg]
-GRing.UnitRing.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitRing.EtaMixin [definition, in mathcomp.algebra.ssralg]
-GRing.UnitRing.Exports [module, in mathcomp.algebra.ssralg]
-GRing.UnitRing.Exports.UnitRingMixin [abbreviation, in mathcomp.algebra.ssralg]
-GRing.UnitRing.Exports.UnitRingType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.UnitRing.Exports.unitRingType [abbreviation, in mathcomp.algebra.ssralg]
-[ unitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-[ unitRingType of _ for _ ] (form_scope) [notation, in mathcomp.algebra.ssralg]
-GRing.UnitRing.inv [projection, in mathcomp.algebra.ssralg]
-GRing.UnitRing.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.UnitRing.Mixin [constructor, in mathcomp.algebra.ssralg]
-GRing.UnitRing.mixin_of [record, in mathcomp.algebra.ssralg]
-GRing.UnitRing.pack [definition, in mathcomp.algebra.ssralg]
-GRing.UnitRing.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.UnitRing.ringType [definition, in mathcomp.algebra.ssralg]
-GRing.UnitRing.sort [projection, in mathcomp.algebra.ssralg]
-GRing.UnitRing.type [record, in mathcomp.algebra.ssralg]
-GRing.UnitRing.unit [projection, in mathcomp.algebra.ssralg]
-GRing.UnitRing.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.UnitRing.zmodType [definition, 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_key [lemma, in mathcomp.algebra.ssralg]
-GRing.valid_QE_proj [definition, in mathcomp.algebra.ssralg]
-GRing.Var [constructor, in mathcomp.algebra.ssralg]
-GRing.wf_QE_proj [definition, in mathcomp.algebra.ssralg]
-GRing.zero [definition, in mathcomp.algebra.ssralg]
-GRing.Zmodule [module, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred [section, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.Add [section, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.Add.addS [variable, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.Add.kS [variable, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.Opp [section, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.Opp.kS [variable, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.Opp.oppS [variable, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.S [variable, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.Sub [section, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.Sub.kS [variable, in mathcomp.algebra.ssralg]
-GRing.ZmodulePred.Sub.subS [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.Zmodule.add [projection, in mathcomp.algebra.ssralg]
-GRing.Zmodule.base [projection, in mathcomp.algebra.ssralg]
-GRing.Zmodule.choiceType [definition, in mathcomp.algebra.ssralg]
-GRing.Zmodule.class [definition, in mathcomp.algebra.ssralg]
-GRing.Zmodule.Class [constructor, in mathcomp.algebra.ssralg]
-GRing.Zmodule.ClassDef [section, in mathcomp.algebra.ssralg]
-GRing.Zmodule.ClassDef.cT [variable, in mathcomp.algebra.ssralg]
-GRing.Zmodule.ClassDef.T [variable, in mathcomp.algebra.ssralg]
-GRing.Zmodule.ClassDef.xT [variable, in mathcomp.algebra.ssralg]
-GRing.Zmodule.class_of [record, in mathcomp.algebra.ssralg]
-GRing.Zmodule.clone [definition, in mathcomp.algebra.ssralg]
-GRing.Zmodule.eqType [definition, in mathcomp.algebra.ssralg]
-GRing.Zmodule.Exports [module, in mathcomp.algebra.ssralg]
-GRing.Zmodule.Exports.ZmodMixin [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Zmodule.Exports.ZmodType [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Zmodule.Exports.zmodType [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.Zmodule.mixin [projection, in mathcomp.algebra.ssralg]
-GRing.Zmodule.Mixin [constructor, in mathcomp.algebra.ssralg]
-GRing.Zmodule.mixin_of [record, in mathcomp.algebra.ssralg]
-GRing.Zmodule.opp [projection, in mathcomp.algebra.ssralg]
-GRing.Zmodule.pack [definition, in mathcomp.algebra.ssralg]
-GRing.Zmodule.Pack [constructor, in mathcomp.algebra.ssralg]
-GRing.Zmodule.sort [projection, in mathcomp.algebra.ssralg]
-GRing.Zmodule.type [record, in mathcomp.algebra.ssralg]
-GRing.Zmodule.xclass [abbreviation, in mathcomp.algebra.ssralg]
-GRing.Zmodule.zero [projection, 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]
-_ \o* _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
-_ \*o _ (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]
-_ %:A (ring_scope) [notation, in mathcomp.algebra.ssralg]
-_ *: _ (ring_scope) [notation, in mathcomp.algebra.ssralg]
-[ char _ ] (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]
-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]
-_ - _ (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]
--%R (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]
-*%R [notation, in mathcomp.algebra.ssralg]
-*:%R [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]
-Group [constructor, in mathcomp.fingroup.fingroup]
-groupAction [record, in mathcomp.fingroup.action]
-GroupAction [constructor, 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.solvable.gseries]
-groupT [abbreviation, in mathcomp.fingroup.fingroup]
-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_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_set_inertia [lemma, in mathcomp.character.inertia]
-group_Ldiv [lemma, in mathcomp.solvable.abelian]
-group_rel_of [definition, in mathcomp.solvable.gseries]
-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_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_finMixin [definition, in mathcomp.fingroup.fingroup]
-group_countMixin [definition, in mathcomp.fingroup.fingroup]
-group_choiceMixin [definition, in mathcomp.fingroup.fingroup]
-group_eqMixin [definition, 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_set_baseGroupMixin [definition, in mathcomp.fingroup.fingroup]
-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_pX1p2 [lemma, in mathcomp.solvable.extraspecial]
-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'_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_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_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]
-gval [projection, in mathcomp.fingroup.fingroup]
-G_ [abbreviation, in mathcomp.solvable.center]
-G' [abbreviation, in mathcomp.solvable.hall]
-G1 [abbreviation, in mathcomp.character.classfun]
-
| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -