From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/index_global_G.html | 335 +++++++++++++++++++-------------------- 1 file changed, 167 insertions(+), 168 deletions(-) (limited to 'docs/htmldoc/index_global_G.html') diff --git a/docs/htmldoc/index_global_G.html b/docs/htmldoc/index_global_G.html index ad61706..83c302a 100644 --- a/docs/htmldoc/index_global_G.html +++ b/docs/htmldoc/index_global_G.html @@ -4,7 +4,7 @@ -mathcomp.ssreflect.tuple +mathcomp.test_suite.hierarchy_test @@ -47,7 +47,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -79,14 +79,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -111,7 +111,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -143,7 +143,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -175,7 +175,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -207,7 +207,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -239,7 +239,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -271,7 +271,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -303,14 +303,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -335,7 +335,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -367,7 +367,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -399,7 +399,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -431,14 +431,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -463,7 +463,7 @@ Z _ other -(185 entries) +(189 entries)

G

@@ -556,8 +556,8 @@ 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]
+'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]
@@ -678,7 +678,6 @@ gcd0z [lemma, in mathcomp.algebra.intdiv]
gcd1n [lemma, in mathcomp.ssreflect.div]
gcd1z [lemma, in mathcomp.algebra.intdiv]
-Gcl [abbreviation, in mathcomp.fingroup.fingroup]
gcore [definition, in mathcomp.fingroup.fingroup]
gcore_max [lemma, in mathcomp.fingroup.fingroup]
gcore_normal [lemma, in mathcomp.fingroup.fingroup]
@@ -707,7 +706,7 @@ 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]
+'K_ _ (ring_scope) [notation, in mathcomp.character.integral_char]
generic_quotient [library]
genGid [lemma, in mathcomp.fingroup.fingroup]
genGidG [lemma, in mathcomp.fingroup.fingroup]
@@ -807,15 +806,15 @@ 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]
+[ 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]
@@ -948,9 +947,9 @@ 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]
+[ 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]
@@ -1003,8 +1002,8 @@ 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]
+[ 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]
@@ -1061,8 +1060,8 @@ 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]
+[ 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]
@@ -1117,8 +1116,8 @@ 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]
+[ 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]
@@ -1147,7 +1146,7 @@ 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]
+[ 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]
@@ -1191,8 +1190,8 @@ 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]
+[ 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]
@@ -1261,7 +1260,7 @@ 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]
+[ 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]
@@ -1335,10 +1334,11 @@ 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]
+[ 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]
@@ -1346,7 +1346,7 @@ 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.mulVx [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]
@@ -1356,6 +1356,7 @@ 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]
@@ -1417,8 +1418,8 @@ 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]
+[ 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]
@@ -1476,8 +1477,8 @@ 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]
+[ 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]
@@ -1489,6 +1490,7 @@ 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]
@@ -1578,15 +1580,15 @@ 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]
+[ 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]
@@ -1614,7 +1616,7 @@ 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]
+*:%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]
@@ -1632,8 +1634,8 @@ 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]
+[ 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]
@@ -1687,9 +1689,9 @@ 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]
+[ 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]
@@ -1994,7 +1996,7 @@ 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]
+_ ^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]
@@ -2012,8 +2014,8 @@ 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]
+[ 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]
@@ -2063,9 +2065,9 @@ 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]
+[ 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]
@@ -2265,15 +2267,15 @@ 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]
+[ 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]
@@ -2375,6 +2377,7 @@ 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]
@@ -2759,6 +2762,7 @@ 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]
@@ -2827,7 +2831,7 @@ 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]
+[ 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]
@@ -2874,8 +2878,8 @@ 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]
+[ 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]
@@ -2940,8 +2944,8 @@ 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]
+[ 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]
@@ -2955,65 +2959,65 @@ 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]
+_ \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]
@@ -3134,11 +3138,6 @@ group0 [lemma, in mathcomp.fingroup.gproduct]
group1 [lemma, in mathcomp.fingroup.fingroup]
group1_contra [lemma, in mathcomp.fingroup.fingroup]
-group1_finType [lemma, in mathcomp.fingroup.fingroup]
-group1_eqType [lemma, in mathcomp.fingroup.fingroup]
-group1_class12 [lemma, in mathcomp.fingroup.fingroup]
-group1_class2 [lemma, in mathcomp.fingroup.fingroup]
-group1_class1 [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]
@@ -3160,12 +3159,12 @@ gtn_min [lemma, in mathcomp.ssreflect.ssrnat]
gtn_max [lemma, in mathcomp.ssreflect.ssrnat]
gtn_eqF [lemma, in mathcomp.ssreflect.ssrnat]
-gTr [abbreviation, in mathcomp.fingroup.fingroup]
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]
@@ -3203,7 +3202,7 @@ Z _ other -(23233 entries) +(23836 entries) Notation Index @@ -3235,14 +3234,14 @@ Z _ other -(1373 entries) +(1409 entries) Module Index A B C -D +D E F G @@ -3267,7 +3266,7 @@ Z _ other -(213 entries) +(221 entries) Variable Index @@ -3299,7 +3298,7 @@ Z _ other -(3475 entries) +(3574 entries) Library Index @@ -3331,7 +3330,7 @@ Z _ other -(89 entries) +(90 entries) Lemma Index @@ -3363,7 +3362,7 @@ Z _ other -(11853 entries) +(12096 entries) Constructor Index @@ -3395,7 +3394,7 @@ Z _ other -(359 entries) +(368 entries) Axiom Index @@ -3427,7 +3426,7 @@ Z _ other -(47 entries) +(45 entries) Inductive Index @@ -3459,14 +3458,14 @@ Z _ other -(103 entries) +(107 entries) Projection Index A B C -D +D E F G @@ -3491,7 +3490,7 @@ Z _ other -(266 entries) +(273 entries) Section Index @@ -3523,7 +3522,7 @@ Z _ other -(1118 entries) +(1140 entries) Abbreviation Index @@ -3555,7 +3554,7 @@ Z _ other -(691 entries) +(728 entries) Definition Index @@ -3587,14 +3586,14 @@ Z _ other -(3461 entries) +(3596 entries) Record Index A B C -D +D E F G @@ -3619,7 +3618,7 @@ Z _ other -(185 entries) +(189 entries) -- cgit v1.2.3