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_F.html | 563 +++++++++++++++++++++++----------------
1 file changed, 333 insertions(+), 230 deletions(-)
(limited to 'docs/htmldoc/index_global_F.html')
diff --git a/docs/htmldoc/index_global_F.html b/docs/htmldoc/index_global_F.html
index 7dfdd53..b27db9e 100644
--- a/docs/htmldoc/index_global_F.html
+++ b/docs/htmldoc/index_global_F.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) |
F
@@ -526,12 +526,12 @@
FalgebraTheory [section, in mathcomp.field.falgebra]
FalgebraTheory.aT [variable, in mathcomp.field.falgebra]
FalgebraTheory.K [variable, in mathcomp.field.falgebra]
-{ aspace _ } (type_scope) [notation, in mathcomp.field.falgebra]
-'Z ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]
-'C ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]
-'C [ _ ] (vspace_scope) [notation, in mathcomp.field.falgebra]
-_ ^+ _ (vspace_scope) [notation, in mathcomp.field.falgebra]
-_ * _ (vspace_scope) [notation, in mathcomp.field.falgebra]
+{ aspace _ } (type_scope) [notation, in mathcomp.field.falgebra]
+'Z ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]
+'C ( _ ) (vspace_scope) [notation, in mathcomp.field.falgebra]
+'C [ _ ] (vspace_scope) [notation, in mathcomp.field.falgebra]
+_ ^+ _ (vspace_scope) [notation, in mathcomp.field.falgebra]
+_ * _ (vspace_scope) [notation, in mathcomp.field.falgebra]
Falgebra_FieldMixin [lemma, in mathcomp.field.falgebra]
Falgebra.algType [definition, in mathcomp.field.falgebra]
Falgebra.BaseMixin [lemma, in mathcomp.field.falgebra]
@@ -555,8 +555,8 @@
Falgebra.Exports [module, in mathcomp.field.falgebra]
Falgebra.Exports.FalgType [abbreviation, in mathcomp.field.falgebra]
Falgebra.Exports.FalgUnitRingType [abbreviation, in mathcomp.field.falgebra]
-[ FalgType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.falgebra]
-[ FalgType _ of _ ] (form_scope) [notation, in mathcomp.field.falgebra]
+[ FalgType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.falgebra]
+[ FalgType _ of _ ] (form_scope) [notation, in mathcomp.field.falgebra]
Falgebra.lalgType [definition, in mathcomp.field.falgebra]
Falgebra.lmodType [definition, in mathcomp.field.falgebra]
Falgebra.mixin [projection, in mathcomp.field.falgebra]
@@ -627,7 +627,6 @@
fcycle [abbreviation, in mathcomp.ssreflect.path]
fE [abbreviation, in mathcomp.fingroup.automorphism]
Fermat's_little_theorem [lemma, in mathcomp.field.finfield]
-fF [abbreviation, in mathcomp.field.closed_field]
ff [abbreviation, in mathcomp.fingroup.morphism]
ffactE [lemma, in mathcomp.ssreflect.binomial]
ffactnn [lemma, in mathcomp.ssreflect.binomial]
@@ -642,7 +641,6 @@
ffact_gt0 [lemma, in mathcomp.ssreflect.binomial]
ffact_rec [definition, in mathcomp.ssreflect.binomial]
ffact0n [lemma, in mathcomp.ssreflect.binomial]
-ffT [abbreviation, in mathcomp.ssreflect.finfun]
fful_lin_char_inj [lemma, in mathcomp.character.character]
ffunE [lemma, in mathcomp.ssreflect.finfun]
ffunK [lemma, in mathcomp.ssreflect.finfun]
@@ -681,10 +679,13 @@
ffun_on [abbreviation, in mathcomp.ssreflect.finfun]
ffun_onP [lemma, in mathcomp.ssreflect.finfun]
ffun_on_mem [definition, in mathcomp.ssreflect.finfun]
+ffun0 [lemma, in mathcomp.ssreflect.finfun]
ffun1_nonzero [lemma, in mathcomp.algebra.ssralg]
fGisom [abbreviation, in mathcomp.fingroup.action]
fgraph [definition, in mathcomp.ssreflect.finfun]
+fgraphK [lemma, in mathcomp.ssreflect.finfun]
fgraph_codom [lemma, in mathcomp.ssreflect.finfun]
+fgraph_ffun0 [lemma, in mathcomp.ssreflect.finfun]
fH [abbreviation, in mathcomp.fingroup.quotient]
fHisom [abbreviation, in mathcomp.fingroup.action]
fH_G [abbreviation, in mathcomp.fingroup.quotient]
@@ -700,7 +701,7 @@
FieldAutomorphism.R [variable, in mathcomp.character.classfun]
FieldAutomorphism.rT [variable, in mathcomp.character.classfun]
FieldAutomorphism.u [variable, in mathcomp.character.classfun]
-_ ^u [notation, in mathcomp.character.classfun]
+_ ^u [notation, in mathcomp.character.classfun]
FieldExt [module, in mathcomp.field.fieldext]
fieldext [library]
FieldExtTheory [section, in mathcomp.field.fieldext]
@@ -739,9 +740,9 @@
FieldExt.eqType [definition, in mathcomp.field.fieldext]
FieldExt.Exports [module, in mathcomp.field.fieldext]
FieldExt.Exports.fieldExtType [abbreviation, in mathcomp.field.fieldext]
-[ fieldExtType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.fieldext]
-[ fieldExtType _ of _ ] (form_scope) [notation, in mathcomp.field.fieldext]
-{ subfield _ } (type_scope) [notation, in mathcomp.field.fieldext]
+[ fieldExtType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.fieldext]
+[ fieldExtType _ of _ ] (form_scope) [notation, in mathcomp.field.fieldext]
+{ subfield _ } (type_scope) [notation, in mathcomp.field.fieldext]
FieldExt.FalgType [definition, in mathcomp.field.fieldext]
FieldExt.Falg_fieldType [definition, in mathcomp.field.fieldext]
FieldExt.Falg_idomainType [definition, in mathcomp.field.fieldext]
@@ -808,7 +809,7 @@
FieldOver.F [variable, in mathcomp.field.fieldext]
FieldOver.F0 [variable, in mathcomp.field.fieldext]
FieldOver.L [variable, in mathcomp.field.fieldext]
-_ *F: _ [notation, in mathcomp.field.fieldext]
+_ *F: _ [notation, in mathcomp.field.fieldext]
FieldRepr [section, in mathcomp.character.mxrepresentation]
FieldRepr.Abelian [section, in mathcomp.character.mxrepresentation]
FieldRepr.AbelianQuotient [section, in mathcomp.character.mxrepresentation]
@@ -848,7 +849,7 @@
FieldRepr.Clifford.sH [variable, in mathcomp.character.mxrepresentation]
FieldRepr.Clifford.sHG [variable, in mathcomp.character.mxrepresentation]
FieldRepr.Clifford.valWact [variable, in mathcomp.character.mxrepresentation]
-'Cl (action_scope) [notation, in mathcomp.character.mxrepresentation]
+'Cl (action_scope) [notation, in mathcomp.character.mxrepresentation]
FieldRepr.Conjugate [section, in mathcomp.character.mxrepresentation]
FieldRepr.Conjugate.B [variable, in mathcomp.character.mxrepresentation]
FieldRepr.Conjugate.G [variable, in mathcomp.character.mxrepresentation]
@@ -960,10 +961,10 @@
FieldRepr.Regular.sG [variable, in mathcomp.character.mxrepresentation]
FieldRepr.Regular.splitG [variable, in mathcomp.character.mxrepresentation]
FieldRepr.Regular.sums_R [variable, in mathcomp.character.mxrepresentation]
-'e_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]
-'R_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]
-'n_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]
-1 (irrType_scope) [notation, in mathcomp.character.mxrepresentation]
+'e_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]
+'R_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]
+'n_ _ (group_ring_scope) [notation, in mathcomp.character.mxrepresentation]
+1 (irrType_scope) [notation, in mathcomp.character.mxrepresentation]
FieldRepr.Similarity [section, in mathcomp.character.mxrepresentation]
FieldRepr.Similarity.G [variable, in mathcomp.character.mxrepresentation]
FieldRepr.Similarity.gT [variable, in mathcomp.character.mxrepresentation]
@@ -981,7 +982,7 @@
FieldRepr.Submodule.rG [variable, in mathcomp.character.mxrepresentation]
FieldRepr.Submodule.U [variable, in mathcomp.character.mxrepresentation]
FieldRepr.Submodule.Umod [variable, in mathcomp.character.mxrepresentation]
-[ 1 _ ] (irrType_scope) [notation, in mathcomp.character.mxrepresentation]
+[ 1 _ ] (irrType_scope) [notation, in mathcomp.character.mxrepresentation]
FieldRoots [section, in mathcomp.algebra.poly]
FieldRoots.F [variable, in mathcomp.algebra.poly]
FieldRoots.UnityRoots [section, in mathcomp.algebra.poly]
@@ -1016,6 +1017,7 @@
filter_pred0 [lemma, in mathcomp.ssreflect.seq]
filter_rcons [lemma, in mathcomp.ssreflect.seq]
filter_cat [lemma, in mathcomp.ssreflect.seq]
+filter_nseq [lemma, in mathcomp.ssreflect.seq]
filter_id [lemma, in mathcomp.ssreflect.seq]
filter_all [lemma, in mathcomp.ssreflect.seq]
filter_pairwise_orthogonal [lemma, in mathcomp.character.classfun]
@@ -1031,6 +1033,9 @@
FinCancel.T [variable, in mathcomp.ssreflect.fintype]
finCharP [lemma, in mathcomp.field.finfield]
find [definition, in mathcomp.ssreflect.seq]
+FinDepTheory [section, in mathcomp.ssreflect.finfun]
+FinDepTheory.aT [variable, in mathcomp.ssreflect.finfun]
+FinDepTheory.rT [variable, in mathcomp.ssreflect.finfun]
findex [definition, in mathcomp.ssreflect.fingraph]
findex_iter [lemma, in mathcomp.ssreflect.fingraph]
findex_max [lemma, in mathcomp.ssreflect.fingraph]
@@ -1043,7 +1048,7 @@
FinDomain.domR [variable, in mathcomp.field.finfield]
FinDomain.lregR [variable, in mathcomp.field.finfield]
FinDomain.R [variable, in mathcomp.field.finfield]
-_ %| _ [notation, in mathcomp.field.finfield]
+_ %| _ [notation, in mathcomp.field.finfield]
find_map [lemma, in mathcomp.ssreflect.seq]
find_nseq [lemma, in mathcomp.ssreflect.seq]
find_cat [lemma, in mathcomp.ssreflect.seq]
@@ -1053,7 +1058,7 @@
finfield [library]
FinFieldExists [section, in mathcomp.field.finfield]
FinFieldExists.map_poly_extField [variable, in mathcomp.field.finfield]
-_ ^%:A (ring_scope) [notation, in mathcomp.field.finfield]
+_ ^%:A (ring_scope) [notation, in mathcomp.field.finfield]
FinFieldExtType [abbreviation, in mathcomp.field.finfield]
FinFieldRepr [section, in mathcomp.character.mxabelem]
FinFieldRepr.F [variable, in mathcomp.character.mxabelem]
@@ -1066,28 +1071,39 @@
FinFieldRepr.ScaleAction [section, in mathcomp.character.mxabelem]
FinFieldRepr.ScaleAction.m [variable, in mathcomp.character.mxabelem]
FinFieldRepr.ScaleAction.n [variable, in mathcomp.character.mxabelem]
-'Zm (action_scope) [notation, in mathcomp.character.mxabelem]
+'Zm (action_scope) [notation, in mathcomp.character.mxabelem]
finField_galois_generator [lemma, in mathcomp.field.finfield]
finField_galois [lemma, in mathcomp.field.finfield]
finField_is_abelem [lemma, in mathcomp.field.finfield]
finField_genPoly [lemma, in mathcomp.field.finfield]
finField_unit [definition, in mathcomp.field.finfield]
FinField.F [variable, in mathcomp.field.finfield]
+Finfun [definition, in mathcomp.ssreflect.finfun]
finfun [abbreviation, in mathcomp.ssreflect.finfun]
-Finfun [constructor, in mathcomp.ssreflect.finfun]
finfun [library]
FinFunComRing [section, in mathcomp.algebra.ssralg]
FinFunComRing.a [variable, in mathcomp.algebra.ssralg]
FinFunComRing.aT [variable, in mathcomp.algebra.ssralg]
FinFunComRing.R [variable, in mathcomp.algebra.ssralg]
+FinfunDef [module, in mathcomp.ssreflect.finfun]
+FinfunDefSig [module, in mathcomp.ssreflect.finfun]
+FinfunDefSig.finfun [axiom, in mathcomp.ssreflect.finfun]
+FinfunDefSig.finfunE [axiom, in mathcomp.ssreflect.finfun]
+FinfunDef.finfun [definition, in mathcomp.ssreflect.finfun]
+FinfunDef.finfunE [lemma, in mathcomp.ssreflect.finfun]
+FinfunK [lemma, in mathcomp.ssreflect.finfun]
FinFunLmod [section, in mathcomp.algebra.ssralg]
FinFunLmod.aT [variable, in mathcomp.algebra.ssralg]
FinFunLmod.R [variable, in mathcomp.algebra.ssralg]
FinFunLmod.rT [variable, in mathcomp.algebra.ssralg]
+FinfunOf [constructor, in mathcomp.ssreflect.finfun]
FinFunRing [section, in mathcomp.algebra.ssralg]
FinFunRing.a [variable, in mathcomp.algebra.ssralg]
FinFunRing.aT [variable, in mathcomp.algebra.ssralg]
FinFunRing.R [variable, in mathcomp.algebra.ssralg]
+FinFunTheory [section, in mathcomp.ssreflect.finfun]
+FinFunTheory.aT [variable, in mathcomp.ssreflect.finfun]
+FinFunTheory.rT [variable, in mathcomp.ssreflect.finfun]
FinFunZmod [section, in mathcomp.algebra.ssralg]
FinFunZmod.aT [variable, in mathcomp.algebra.ssralg]
FinFunZmod.rT [variable, in mathcomp.algebra.ssralg]
@@ -1096,13 +1112,12 @@
FinFunZmod.Sum.I [variable, in mathcomp.algebra.ssralg]
FinFunZmod.Sum.P [variable, in mathcomp.algebra.ssralg]
FinFunZmod.Sum.r [variable, in mathcomp.algebra.ssralg]
-finfun_finMixin [definition, in mathcomp.ssreflect.finfun]
-finfun_countMixin [definition, in mathcomp.ssreflect.finfun]
-finfun_choiceMixin [definition, in mathcomp.ssreflect.finfun]
-finfun_eqMixin [definition, in mathcomp.ssreflect.finfun]
finfun_def [abbreviation, in mathcomp.ssreflect.finfun]
-finfun_of [definition, in mathcomp.ssreflect.finfun]
-finfun_type [inductive, in mathcomp.ssreflect.finfun]
+finfun_of [inductive, in mathcomp.ssreflect.finfun]
+finfun_rec [definition, in mathcomp.ssreflect.finfun]
+finfun_cons [constructor, in mathcomp.ssreflect.finfun]
+finfun_nil [constructor, in mathcomp.ssreflect.finfun]
+finfun_on [inductive, in mathcomp.ssreflect.finfun]
finfun_of_set [definition, in mathcomp.ssreflect.finset]
fingraph [library]
FinGroup [module, in mathcomp.fingroup.fingroup]
@@ -1123,8 +1138,8 @@
FinGroup.Exports.baseFinGroupType [abbreviation, in mathcomp.fingroup.fingroup]
FinGroup.Exports.FinGroupType [abbreviation, in mathcomp.fingroup.fingroup]
FinGroup.Exports.finGroupType [abbreviation, in mathcomp.fingroup.fingroup]
-[ finGroupType of _ ] (form_scope) [notation, in mathcomp.fingroup.fingroup]
-[ baseFinGroupType of _ ] (form_scope) [notation, in mathcomp.fingroup.fingroup]
+[ finGroupType of _ ] (form_scope) [notation, in mathcomp.fingroup.fingroup]
+[ baseFinGroupType of _ ] (form_scope) [notation, in mathcomp.fingroup.fingroup]
FinGroup.finClass [definition, in mathcomp.fingroup.fingroup]
FinGroup.InheritedClasses [section, in mathcomp.fingroup.fingroup]
FinGroup.InheritedClasses.bT [variable, in mathcomp.fingroup.fingroup]
@@ -1140,9 +1155,9 @@
FinGroup.Mixin.mul1 [variable, in mathcomp.fingroup.fingroup]
FinGroup.Mixin.one [variable, in mathcomp.fingroup.fingroup]
FinGroup.Mixin.T [variable, in mathcomp.fingroup.fingroup]
-_ ^-1 [notation, in mathcomp.fingroup.fingroup]
-_ * _ [notation, in mathcomp.fingroup.fingroup]
-1 [notation, in mathcomp.fingroup.fingroup]
+_ ^-1 [notation, in mathcomp.fingroup.fingroup]
+_ * _ [notation, in mathcomp.fingroup.fingroup]
+1 [notation, in mathcomp.fingroup.fingroup]
FinGroup.mk_invMg [lemma, in mathcomp.fingroup.fingroup]
FinGroup.mk_invgK [lemma, in mathcomp.fingroup.fingroup]
FinGroup.mul [projection, in mathcomp.fingroup.fingroup]
@@ -1209,13 +1224,13 @@
FiniteModule.OneFinMod.f2sub [variable, in mathcomp.solvable.finmodule]
FiniteModule.OneFinMod.gT [variable, in mathcomp.solvable.finmodule]
FiniteModule.OneFinMod.sub2f [variable, in mathcomp.solvable.finmodule]
-'M (action_scope) [notation, in mathcomp.solvable.finmodule]
-'M (groupAction_scope) [notation, in mathcomp.solvable.finmodule]
-_ ^@ _ (ring_scope) [notation, in mathcomp.solvable.finmodule]
+'M (action_scope) [notation, in mathcomp.solvable.finmodule]
+'M (groupAction_scope) [notation, in mathcomp.solvable.finmodule]
+_ ^@ _ (ring_scope) [notation, in mathcomp.solvable.finmodule]
FiniteModule.valA [abbreviation, in mathcomp.solvable.finmodule]
-'M (action_scope) [notation, in mathcomp.solvable.finmodule]
-'M (groupAction_scope) [notation, in mathcomp.solvable.finmodule]
-_ ^@ _ (ring_scope) [notation, in mathcomp.solvable.finmodule]
+'M (action_scope) [notation, in mathcomp.solvable.finmodule]
+'M (groupAction_scope) [notation, in mathcomp.solvable.finmodule]
+_ ^@ _ (ring_scope) [notation, in mathcomp.solvable.finmodule]
FiniteQuant [module, in mathcomp.ssreflect.fintype]
FiniteQuant.all [definition, in mathcomp.ssreflect.fintype]
FiniteQuant.all_in [definition, in mathcomp.ssreflect.fintype]
@@ -1223,39 +1238,39 @@
FiniteQuant.Definitions.T [variable, in mathcomp.ssreflect.fintype]
FiniteQuant.ex [definition, in mathcomp.ssreflect.fintype]
FiniteQuant.Exports [module, in mathcomp.ssreflect.fintype]
-, exists _ : _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-, exists _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ exists _ : _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ exists _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ exists ( _ : _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ exists ( _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ exists _ : _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ exists _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-, forall _ : _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-, forall _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ forall _ : _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ forall _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ forall ( _ : _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ forall ( _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ forall _ : _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-[ forall _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
-, exists ( _ : _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
-, exists ( _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
-, exists _ : _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
-, exists _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
-, forall ( _ : _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
-, forall ( _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
-, forall _ : _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
-, forall _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
-, _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists _ : _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists _ : _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists ( _ : _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists ( _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists _ : _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ exists _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall _ : _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall _ in _ _ (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall _ : _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall _ in _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall ( _ : _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall ( _ | _ ) _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall _ : _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+[ forall _ _ ] (bool_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists ( _ : _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists ( _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists _ : _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, exists _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall ( _ : _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall ( _ | _ ) _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall _ : _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, forall _ _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
+, _ (fin_quant_scope) [notation, in mathcomp.ssreflect.fintype]
FiniteQuant.ex_in [definition, in mathcomp.ssreflect.fintype]
FiniteQuant.Quantified [constructor, in mathcomp.ssreflect.fintype]
FiniteQuant.quantified [inductive, in mathcomp.ssreflect.fintype]
FiniteQuant.quant0b [definition, in mathcomp.ssreflect.fintype]
-_ ^~ [notation, in mathcomp.ssreflect.fintype]
-_ ^* [notation, in mathcomp.ssreflect.fintype]
-[ _ : _ | _ ] [notation, in mathcomp.ssreflect.fintype]
-[ _ | _ ] [notation, in mathcomp.ssreflect.fintype]
+_ ^~ [notation, in mathcomp.ssreflect.fintype]
+_ ^* [notation, in mathcomp.ssreflect.fintype]
+[ _ : _ | _ ] [notation, in mathcomp.ssreflect.fintype]
+[ _ | _ ] [notation, in mathcomp.ssreflect.fintype]
finite_PET [lemma, in mathcomp.field.separable]
Finite.axiom [definition, in mathcomp.ssreflect.fintype]
Finite.base [projection, in mathcomp.ssreflect.fintype]
@@ -1287,8 +1302,8 @@
Finite.Exports.FinType [abbreviation, in mathcomp.ssreflect.fintype]
Finite.Exports.finType [abbreviation, in mathcomp.ssreflect.fintype]
Finite.Exports.UniqFinMixin [abbreviation, in mathcomp.ssreflect.fintype]
-[ finType of _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
-[ finType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
+[ finType of _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
+[ finType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
Finite.mixin [projection, in mathcomp.ssreflect.fintype]
Finite.Mixin [constructor, in mathcomp.ssreflect.fintype]
Finite.Mixins [section, in mathcomp.ssreflect.fintype]
@@ -1307,7 +1322,9 @@
Finite.UniqMixin [definition, in mathcomp.ssreflect.fintype]
Finite.uniq_enumP [lemma, in mathcomp.ssreflect.fintype]
Finite.xclass [abbreviation, in mathcomp.ssreflect.fintype]
+finMixin [definition, in mathcomp.ssreflect.finfun]
finmodule [library]
+finPi [abbreviation, in mathcomp.ssreflect.finfun]
FinRing [section, in mathcomp.field.finfield]
FinRing [module, in mathcomp.algebra.finalg]
FinRingRepr [section, in mathcomp.character.mxabelem]
@@ -1322,6 +1339,16 @@
FinRing.AdditiveGroup.U [variable, in mathcomp.algebra.finalg]
FinRing.Algebra [module, in mathcomp.algebra.finalg]
FinRing.Algebra.algType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_countRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_countZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_countType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.base [projection, in mathcomp.algebra.finalg]
FinRing.Algebra.baseFinGroupType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.base2 [definition, in mathcomp.algebra.finalg]
@@ -1334,24 +1361,19 @@
FinRing.Algebra.ClassDef.R [variable, in mathcomp.algebra.finalg]
FinRing.Algebra.ClassDef.xT [variable, in mathcomp.algebra.finalg]
FinRing.Algebra.class_of [record, in mathcomp.algebra.finalg]
+FinRing.Algebra.countRingType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Algebra.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.eqType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.Exports [module, in mathcomp.algebra.finalg]
FinRing.Algebra.Exports.finAlgType [abbreviation, in mathcomp.algebra.finalg]
-[ finAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.Algebra.finGroupType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.finLalgType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.finLmodType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.finRingType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.finType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finLalgType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finLmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.lalgType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.lmodType [definition, in mathcomp.algebra.finalg]
FinRing.Algebra.mixin [projection, in mathcomp.algebra.finalg]
@@ -1366,7 +1388,6 @@
FinRing.ComRing [module, in mathcomp.algebra.finalg]
FinRing.ComRing.base [projection, in mathcomp.algebra.finalg]
FinRing.ComRing.baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.base2 [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.choiceType [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.class [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.Class [constructor, in mathcomp.algebra.finalg]
@@ -1375,20 +1396,28 @@
FinRing.ComRing.ClassDef.xT [variable, in mathcomp.algebra.finalg]
FinRing.ComRing.class_of [record, in mathcomp.algebra.finalg]
FinRing.ComRing.comRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_finType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_finType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.countRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.countType [definition, in mathcomp.algebra.finalg]
+FinRing.ComRing.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.eqType [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.Exports [module, in mathcomp.algebra.finalg]
FinRing.ComRing.Exports.finComRingType [abbreviation, in mathcomp.algebra.finalg]
-[ finComRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finComRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.ComRing.finGroupType [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.finRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.finType [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.join_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.ComRing.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.mixin [projection, in mathcomp.algebra.finalg]
FinRing.ComRing.pack [definition, in mathcomp.algebra.finalg]
FinRing.ComRing.Pack [constructor, in mathcomp.algebra.finalg]
@@ -1400,10 +1429,7 @@
FinRing.ComUnitRing [module, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.base [projection, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.base2 [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.base3 [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.choiceType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.cjoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.class [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.Class [constructor, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.ClassDef [section, in mathcomp.algebra.finalg]
@@ -1411,34 +1437,49 @@
FinRing.ComUnitRing.ClassDef.xT [variable, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.class_of [record, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.comRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comRing_finUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.comUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComRing_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.countType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countUnitRing_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.eqType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.Exports [module, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.Exports.finComUnitRingType [abbreviation, in mathcomp.algebra.finalg]
-[ finComUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.fcjoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+[ finComUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.finComRing_finUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finGroupType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.mixin [projection, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.pack [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.Pack [constructor, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.ringType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.sort [projection, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.type [record, in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.ujoin_finComRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.unitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.unitRing_finComRingType [definition, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.xclass [abbreviation, in mathcomp.algebra.finalg]
FinRing.ComUnitRing.zmodType [definition, in mathcomp.algebra.finalg]
FinRing.DecField [module, in mathcomp.algebra.finalg]
@@ -1465,7 +1506,6 @@
FinRing.Field [module, in mathcomp.algebra.finalg]
FinRing.Field.base [projection, in mathcomp.algebra.finalg]
FinRing.Field.baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.base2 [definition, in mathcomp.algebra.finalg]
FinRing.Field.choiceType [definition, in mathcomp.algebra.finalg]
FinRing.Field.class [definition, in mathcomp.algebra.finalg]
FinRing.Field.Class [constructor, in mathcomp.algebra.finalg]
@@ -1475,12 +1515,37 @@
FinRing.Field.class_of [record, in mathcomp.algebra.finalg]
FinRing.Field.comRingType [definition, in mathcomp.algebra.finalg]
FinRing.Field.comUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countFieldType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countField_finIdomainType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countField_finComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countField_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countField_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countField_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countField_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countField_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countField_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countField_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countIdomainType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countRingType [definition, in mathcomp.algebra.finalg]
FinRing.Field.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.Field.eqType [definition, in mathcomp.algebra.finalg]
FinRing.Field.Exports [module, in mathcomp.algebra.finalg]
FinRing.Field.Exports.finFieldType [abbreviation, in mathcomp.algebra.finalg]
-[ finFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finFieldType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.Field.fieldType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.field_finIdomainType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.field_finComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.field_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.field_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.field_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.field_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.field_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.field_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Field.field_finType [definition, in mathcomp.algebra.finalg]
FinRing.Field.finComRingType [definition, in mathcomp.algebra.finalg]
FinRing.Field.finComUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.Field.finGroupType [definition, in mathcomp.algebra.finalg]
@@ -1490,15 +1555,6 @@
FinRing.Field.finUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.Field.finZmodType [definition, in mathcomp.algebra.finalg]
FinRing.Field.idomainType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.join_finIdomainType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.join_finComUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.join_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.join_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.join_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Field.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.Field.mixin [projection, in mathcomp.algebra.finalg]
FinRing.Field.pack [definition, in mathcomp.algebra.finalg]
FinRing.Field.Pack [constructor, in mathcomp.algebra.finalg]
@@ -1525,7 +1581,6 @@
FinRing.IntegralDomain [module, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.base [projection, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.base2 [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.choiceType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.class [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.Class [constructor, in mathcomp.algebra.finalg]
@@ -1535,11 +1590,25 @@
FinRing.IntegralDomain.class_of [record, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.comRingType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.comUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomainType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countRingType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.countType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.eqType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.Exports [module, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.Exports.finIdomainType [abbreviation, in mathcomp.algebra.finalg]
-[ finIdomainType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finIdomainType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.finComRingType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.finComUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.finGroupType [definition, in mathcomp.algebra.finalg]
@@ -1548,14 +1617,14 @@
FinRing.IntegralDomain.finUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.finZmodType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.idomainType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finComUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finComRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finComUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finComRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finType [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.mixin [projection, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.pack [definition, in mathcomp.algebra.finalg]
FinRing.IntegralDomain.Pack [constructor, in mathcomp.algebra.finalg]
@@ -1579,31 +1648,38 @@
FinRing.Lalgebra.ClassDef.R [variable, in mathcomp.algebra.finalg]
FinRing.Lalgebra.ClassDef.xT [variable, in mathcomp.algebra.finalg]
FinRing.Lalgebra.class_of [record, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.countRingType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.eqType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.Exports [module, in mathcomp.algebra.finalg]
FinRing.Lalgebra.Exports.finLalgType [abbreviation, in mathcomp.algebra.finalg]
-[ finLalgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finLalgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.Lalgebra.finGroupType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finLmod_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finLmod_countRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finLmod_ringType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.finRingType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.finType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.fljoin_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finLmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.lalgType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.ljoin_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_countRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_countZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_countType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.lmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lmod_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lmod_countRingType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.mixin [projection, in mathcomp.algebra.finalg]
FinRing.Lalgebra.pack [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.Pack [constructor, in mathcomp.algebra.finalg]
FinRing.Lalgebra.ringType [definition, in mathcomp.algebra.finalg]
-FinRing.Lalgebra.rjoin_finLmodType [definition, in mathcomp.algebra.finalg]
FinRing.Lalgebra.sort [projection, in mathcomp.algebra.finalg]
FinRing.Lalgebra.type [record, in mathcomp.algebra.finalg]
FinRing.Lalgebra.xclass [abbreviation, in mathcomp.algebra.finalg]
@@ -1611,7 +1687,6 @@
FinRing.Lmodule [module, in mathcomp.algebra.finalg]
FinRing.Lmodule.base [projection, in mathcomp.algebra.finalg]
FinRing.Lmodule.baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.base2 [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.choiceType [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.class [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.Class [constructor, in mathcomp.algebra.finalg]
@@ -1622,18 +1697,21 @@
FinRing.Lmodule.ClassDef.xT [variable, in mathcomp.algebra.finalg]
FinRing.Lmodule.class_of [record, in mathcomp.algebra.finalg]
FinRing.Lmodule.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.eqType [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.Exports [module, in mathcomp.algebra.finalg]
FinRing.Lmodule.Exports.finLmodType [abbreviation, in mathcomp.algebra.finalg]
-[ finLmodType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finLmodType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.Lmodule.finGroupType [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.finType [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Lmodule.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.lmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_countZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_finType [definition, in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_countType [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.mixin [projection, in mathcomp.algebra.finalg]
FinRing.Lmodule.pack [definition, in mathcomp.algebra.finalg]
FinRing.Lmodule.Pack [constructor, in mathcomp.algebra.finalg]
@@ -1646,7 +1724,6 @@
FinRing.Ring [module, in mathcomp.algebra.finalg]
FinRing.Ring.base [projection, in mathcomp.algebra.finalg]
FinRing.Ring.baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.base2 [definition, in mathcomp.algebra.finalg]
FinRing.Ring.choiceType [definition, in mathcomp.algebra.finalg]
FinRing.Ring.class [definition, in mathcomp.algebra.finalg]
FinRing.Ring.Class [constructor, in mathcomp.algebra.finalg]
@@ -1654,11 +1731,17 @@
FinRing.Ring.ClassDef.cT [variable, in mathcomp.algebra.finalg]
FinRing.Ring.ClassDef.xT [variable, in mathcomp.algebra.finalg]
FinRing.Ring.class_of [record, in mathcomp.algebra.finalg]
+FinRing.Ring.countRingType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.countRing_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.countRing_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.countRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.countRing_finType [definition, in mathcomp.algebra.finalg]
FinRing.Ring.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.Ring.eqType [definition, in mathcomp.algebra.finalg]
FinRing.Ring.Exports [module, in mathcomp.algebra.finalg]
FinRing.Ring.Exports.finRingType [abbreviation, in mathcomp.algebra.finalg]
-[ finRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.Ring.finGroupType [definition, in mathcomp.algebra.finalg]
FinRing.Ring.finType [definition, in mathcomp.algebra.finalg]
FinRing.Ring.finZmodType [definition, in mathcomp.algebra.finalg]
@@ -1666,16 +1749,16 @@
FinRing.Ring.inv [definition, in mathcomp.algebra.finalg]
FinRing.Ring.invr_out [lemma, in mathcomp.algebra.finalg]
FinRing.Ring.is_inv [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.Ring.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.Ring.mixin [projection, in mathcomp.algebra.finalg]
FinRing.Ring.mulrV [lemma, in mathcomp.algebra.finalg]
FinRing.Ring.mulVr [lemma, in mathcomp.algebra.finalg]
FinRing.Ring.pack [definition, in mathcomp.algebra.finalg]
FinRing.Ring.Pack [constructor, in mathcomp.algebra.finalg]
FinRing.Ring.ringType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.ring_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.ring_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.ring_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Ring.ring_finType [definition, in mathcomp.algebra.finalg]
FinRing.Ring.sort [projection, in mathcomp.algebra.finalg]
FinRing.Ring.type [record, in mathcomp.algebra.finalg]
FinRing.Ring.unit [definition, in mathcomp.algebra.finalg]
@@ -1700,7 +1783,6 @@
FinRing.unit [abbreviation, in mathcomp.algebra.finalg]
FinRing.Unit [constructor, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra [module, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ajoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.algType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.base [projection, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.baseFinGroupType [definition, in mathcomp.algebra.finalg]
@@ -1715,12 +1797,20 @@
FinRing.UnitAlgebra.ClassDef.R [variable, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.ClassDef.xT [variable, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.class_of [record, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countRingType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.countType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_finAlgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_algType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_lalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_lmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.eqType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.Exports [module, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.Exports.finUnitAlgType [abbreviation, in mathcomp.algebra.finalg]
-[ finUnitAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.fajoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
+[ finUnitAlgType _ of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finAlgType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finGroupType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finLalgType [definition, in mathcomp.algebra.finalg]
@@ -1728,39 +1818,44 @@
FinRing.UnitAlgebra.finRingType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_finAlgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_algType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_lalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_lmodType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.fljoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.fnjoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finAlgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finLalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finLmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finUnitRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.lalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ljoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.lmodType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.mixin [projection, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.njoin_finUnitRingType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.pack [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.Pack [constructor, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.ringType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.sort [projection, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.type [record, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ujoin_finAlgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ujoin_finLalgType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ujoin_finLmodType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.unitAlgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finAlgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finLmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_countUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_countRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_countZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_countType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.unitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitRing_finAlgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitRing_finLalgType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitRing_finLmodType [definition, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.xclass [abbreviation, in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.zmodType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing [module, in mathcomp.algebra.finalg]
FinRing.UnitRing.base [projection, in mathcomp.algebra.finalg]
FinRing.UnitRing.baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.base2 [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.choiceType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.class [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.Class [constructor, in mathcomp.algebra.finalg]
@@ -1768,20 +1863,23 @@
FinRing.UnitRing.ClassDef.cT [variable, in mathcomp.algebra.finalg]
FinRing.UnitRing.ClassDef.xT [variable, in mathcomp.algebra.finalg]
FinRing.UnitRing.class_of [record, in mathcomp.algebra.finalg]
+FinRing.UnitRing.countRingType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.countType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_finType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.countZmodType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.eqType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.Exports [module, in mathcomp.algebra.finalg]
FinRing.UnitRing.Exports.finUnitRingType [abbreviation, in mathcomp.algebra.finalg]
-[ finUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finUnitRingType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.UnitRing.finGroupType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.finRingType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.finType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_finRingType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_finZmodType [definition, in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.mixin [projection, in mathcomp.algebra.finalg]
FinRing.UnitRing.pack [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.Pack [constructor, in mathcomp.algebra.finalg]
@@ -1789,6 +1887,11 @@
FinRing.UnitRing.sort [projection, in mathcomp.algebra.finalg]
FinRing.UnitRing.type [record, in mathcomp.algebra.finalg]
FinRing.UnitRing.unitRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_finRingType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_finZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_finType [definition, in mathcomp.algebra.finalg]
FinRing.UnitRing.xclass [abbreviation, in mathcomp.algebra.finalg]
FinRing.UnitRing.zmodType [definition, in mathcomp.algebra.finalg]
FinRing.UnitsGroup [section, in mathcomp.algebra.finalg]
@@ -1830,17 +1933,18 @@
FinRing.Zmodule.ClassDef.xT [variable, in mathcomp.algebra.finalg]
FinRing.Zmodule.class_of [record, in mathcomp.algebra.finalg]
FinRing.Zmodule.countType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.countZmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.countZmod_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.countZmod_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.countZmod_finType [definition, in mathcomp.algebra.finalg]
FinRing.Zmodule.eqType [definition, in mathcomp.algebra.finalg]
FinRing.Zmodule.Exports [module, in mathcomp.algebra.finalg]
FinRing.Zmodule.Exports.finZmodType [abbreviation, in mathcomp.algebra.finalg]
-[ finGroupType of _ for +%R ] (form_scope) [notation, in mathcomp.algebra.finalg]
-[ baseFinGroupType of _ for +%R ] (form_scope) [notation, in mathcomp.algebra.finalg]
-[ finZmodType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finGroupType of _ for +%R ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ baseFinGroupType of _ for +%R ] (form_scope) [notation, in mathcomp.algebra.finalg]
+[ finZmodType of _ ] (form_scope) [notation, in mathcomp.algebra.finalg]
FinRing.Zmodule.finGroupType [definition, in mathcomp.algebra.finalg]
FinRing.Zmodule.finType [definition, in mathcomp.algebra.finalg]
-FinRing.Zmodule.join_finGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Zmodule.join_baseFinGroupType [definition, in mathcomp.algebra.finalg]
-FinRing.Zmodule.join_finType [definition, in mathcomp.algebra.finalg]
FinRing.Zmodule.mixin [projection, in mathcomp.algebra.finalg]
FinRing.Zmodule.pack [definition, in mathcomp.algebra.finalg]
FinRing.Zmodule.Pack [constructor, in mathcomp.algebra.finalg]
@@ -1848,6 +1952,9 @@
FinRing.Zmodule.type [record, in mathcomp.algebra.finalg]
FinRing.Zmodule.xclass [abbreviation, in mathcomp.algebra.finalg]
FinRing.Zmodule.zmodType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.zmod_finGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.zmod_baseFinGroupType [definition, in mathcomp.algebra.finalg]
+FinRing.Zmodule.zmod_finType [definition, in mathcomp.algebra.finalg]
FinRing.zmodVgE [lemma, in mathcomp.algebra.finalg]
FinRing.zmodXgE [lemma, in mathcomp.algebra.finalg]
FinRing.zmod_abelian [lemma, in mathcomp.algebra.finalg]
@@ -1866,9 +1973,6 @@
FinSplittingField.FinGalois.galL [variable, in mathcomp.field.finfield]
FinSplittingField.FinGalois.L [variable, in mathcomp.field.finfield]
FinSplittingField.order [variable, in mathcomp.field.finfield]
-FinTheory [section, in mathcomp.ssreflect.finfun]
-FinTheory.aT [variable, in mathcomp.ssreflect.finfun]
-FinTheory.rT [variable, in mathcomp.ssreflect.finfun]
FinTuple [module, in mathcomp.ssreflect.tuple]
FinTupleSig [module, in mathcomp.ssreflect.tuple]
FinTupleSig.enum [axiom, in mathcomp.ssreflect.tuple]
@@ -2001,13 +2105,16 @@
fmorph_unity_root [lemma, in mathcomp.algebra.poly]
fmorph_root [lemma, in mathcomp.algebra.poly]
foldl [definition, in mathcomp.ssreflect.seq]
+foldlE [lemma, in mathcomp.ssreflect.bigop]
FoldLeft [section, in mathcomp.ssreflect.seq]
FoldLeft.f [variable, in mathcomp.ssreflect.seq]
FoldLeft.R [variable, in mathcomp.ssreflect.seq]
FoldLeft.T [variable, in mathcomp.ssreflect.seq]
foldl_cat [lemma, in mathcomp.ssreflect.seq]
foldl_rev [lemma, in mathcomp.ssreflect.seq]
+foldl_idx [lemma, in mathcomp.ssreflect.bigop]
foldr [definition, in mathcomp.ssreflect.seq]
+foldrE [lemma, in mathcomp.ssreflect.bigop]
FoldRight [section, in mathcomp.ssreflect.seq]
FoldRightComp [section, in mathcomp.ssreflect.seq]
FoldRightComp.f [variable, in mathcomp.ssreflect.seq]
@@ -2025,6 +2132,7 @@
forallb_tnth [lemma, in mathcomp.ssreflect.tuple]
forallP [lemma, in mathcomp.ssreflect.fintype]
forallPP [lemma, in mathcomp.ssreflect.fintype]
+forall_inPP [lemma, in mathcomp.ssreflect.fintype]
forall_inP [lemma, in mathcomp.ssreflect.fintype]
fp [abbreviation, in mathcomp.algebra.mxpoly]
fp [abbreviation, in mathcomp.algebra.mxpoly]
@@ -2044,11 +2152,11 @@
frac [projection, in mathcomp.algebra.fraction]
FracDomain [section, in mathcomp.algebra.fraction]
FracDomain.R [variable, in mathcomp.algebra.fraction]
-{ ratio _ } [notation, in mathcomp.algebra.fraction]
+{ ratio _ } [notation, in mathcomp.algebra.fraction]
FracField [module, in mathcomp.algebra.fraction]
FracFieldTheory [section, in mathcomp.algebra.fraction]
FracFieldTheory.R [variable, in mathcomp.algebra.fraction]
-_ %:F [notation, in mathcomp.algebra.fraction]
+_ %:F [notation, in mathcomp.algebra.fraction]
FracField.add [definition, in mathcomp.algebra.fraction]
FracField.addA [lemma, in mathcomp.algebra.fraction]
FracField.addC [lemma, in mathcomp.algebra.fraction]
@@ -2070,8 +2178,8 @@
FracField.frac [abbreviation, in mathcomp.algebra.fraction]
FracField.FracField [section, in mathcomp.algebra.fraction]
FracField.FracField.R [variable, in mathcomp.algebra.fraction]
-_ %:F [notation, in mathcomp.algebra.fraction]
-{ fraction _ } [notation, in mathcomp.algebra.fraction]
+_ %:F [notation, in mathcomp.algebra.fraction]
+{ fraction _ } [notation, in mathcomp.algebra.fraction]
FracField.frac_comRingMixin [definition, in mathcomp.algebra.fraction]
FracField.frac_zmodMixin [definition, in mathcomp.algebra.fraction]
FracField.inv [definition, in mathcomp.algebra.fraction]
@@ -2205,6 +2313,8 @@
fT [abbreviation, in mathcomp.ssreflect.finfun]
fT [abbreviation, in mathcomp.ssreflect.finfun]
fT [abbreviation, in mathcomp.ssreflect.finfun]
+fT [abbreviation, in mathcomp.ssreflect.finfun]
+fT [abbreviation, in mathcomp.ssreflect.finfun]
fullv [definition, in mathcomp.algebra.vector]
FunctorGroup [section, in mathcomp.solvable.gfunctor]
FunctorGroup.F [variable, in mathcomp.solvable.gfunctor]
@@ -2218,16 +2328,6 @@
FunctorTheory.F [variable, in mathcomp.solvable.gfunctor]
Fundamental_Theorem_of_Algebraics [lemma, in mathcomp.field.algebraics_fundamentals]
FunDelta [constructor, in mathcomp.ssreflect.eqtype]
-FunFinfun [module, in mathcomp.ssreflect.finfun]
-FunFinfunSig [module, in mathcomp.ssreflect.finfun]
-FunFinfunSig.finfun [axiom, in mathcomp.ssreflect.finfun]
-FunFinfunSig.finfunE [axiom, in mathcomp.ssreflect.finfun]
-FunFinfunSig.fun_of_finE [axiom, in mathcomp.ssreflect.finfun]
-FunFinfunSig.fun_of_fin [axiom, in mathcomp.ssreflect.finfun]
-FunFinfun.finfun [definition, in mathcomp.ssreflect.finfun]
-FunFinfun.finfunE [lemma, in mathcomp.ssreflect.finfun]
-FunFinfun.fun_of_finE [lemma, in mathcomp.ssreflect.finfun]
-FunFinfun.fun_of_fin [definition, in mathcomp.ssreflect.finfun]
FunImage [section, in mathcomp.ssreflect.finset]
FunImageComp [section, in mathcomp.ssreflect.finset]
FunImageComp.T [variable, in mathcomp.ssreflect.finset]
@@ -2240,6 +2340,9 @@
FunImage.ImsetTheory.ImsetProp.f [variable, in mathcomp.ssreflect.finset]
FunImage.ImsetTheory.ImsetProp.f2 [variable, in mathcomp.ssreflect.finset]
FunImage.ImsetTheory.rT [variable, in mathcomp.ssreflect.finset]
+FunPlainTheory [section, in mathcomp.ssreflect.finfun]
+FunPlainTheory.aT [variable, in mathcomp.ssreflect.finfun]
+FunPlainTheory.rT [variable, in mathcomp.ssreflect.finfun]
FunVectType [section, in mathcomp.algebra.vector]
FunVectType.I [variable, in mathcomp.algebra.vector]
FunVectType.R [variable, in mathcomp.algebra.vector]
@@ -2255,8 +2358,8 @@
fun_of_lfun_def [definition, in mathcomp.algebra.vector]
fun_of_matrix [definition, in mathcomp.algebra.matrix]
fun_of_cfun [definition, in mathcomp.character.classfun]
-fun_of_fin [abbreviation, in mathcomp.ssreflect.finfun]
-fun_of_fin_def [abbreviation, in mathcomp.ssreflect.finfun]
+fun_of_fin [definition, in mathcomp.ssreflect.finfun]
+fun_of_fin_rec [definition, in mathcomp.ssreflect.finfun]
fun_delta [inductive, in mathcomp.ssreflect.eqtype]
fun_adjunction [abbreviation, in mathcomp.ssreflect.fingraph]
Fun2Set1 [section, in mathcomp.ssreflect.finset]
@@ -2337,7 +2440,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -2369,14 +2472,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -2401,7 +2504,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -2433,7 +2536,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -2465,7 +2568,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -2497,7 +2600,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -2529,7 +2632,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -2561,7 +2664,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -2593,14 +2696,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -2625,7 +2728,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -2657,7 +2760,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -2689,7 +2792,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -2721,14 +2824,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -2753,7 +2856,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
--
cgit v1.2.3