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_definition_F.html | 353 ++++++++++++++++++++++-------------
1 file changed, 221 insertions(+), 132 deletions(-)
(limited to 'docs/htmldoc/index_definition_F.html')
diff --git a/docs/htmldoc/index_definition_F.html b/docs/htmldoc/index_definition_F.html
index 179caa4..3c940c8 100644
--- a/docs/htmldoc/index_definition_F.html
+++ b/docs/htmldoc/index_definition_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 (definition)
@@ -570,11 +570,9 @@
FinDomainFieldType [in mathcomp.field.finfield]
FinDomainSplittingFieldType [in mathcomp.field.finfield]
finField_unit [in mathcomp.field.finfield]
-finfun_finMixin [in mathcomp.ssreflect.finfun]
-finfun_countMixin [in mathcomp.ssreflect.finfun]
-finfun_choiceMixin [in mathcomp.ssreflect.finfun]
-finfun_eqMixin [in mathcomp.ssreflect.finfun]
-finfun_of [in mathcomp.ssreflect.finfun]
+Finfun [in mathcomp.ssreflect.finfun]
+FinfunDef.finfun [in mathcomp.ssreflect.finfun]
+finfun_rec [in mathcomp.ssreflect.finfun]
finfun_of_set [in mathcomp.ssreflect.finset]
FinGroup.arg_finType [in mathcomp.fingroup.fingroup]
FinGroup.arg_countType [in mathcomp.fingroup.fingroup]
@@ -618,12 +616,25 @@
Finite.eqType [in mathcomp.ssreflect.fintype]
Finite.pack [in mathcomp.ssreflect.fintype]
Finite.UniqMixin [in mathcomp.ssreflect.fintype]
+finMixin [in mathcomp.ssreflect.finfun]
FinRing.Algebra.algType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finLalgType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finLmodType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finRingType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_countRingType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finZmodType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_countZmodType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finGroupType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_finType [in mathcomp.algebra.finalg]
+FinRing.Algebra.alg_countType [in mathcomp.algebra.finalg]
FinRing.Algebra.baseFinGroupType [in mathcomp.algebra.finalg]
FinRing.Algebra.base2 [in mathcomp.algebra.finalg]
FinRing.Algebra.choiceType [in mathcomp.algebra.finalg]
FinRing.Algebra.class [in mathcomp.algebra.finalg]
+FinRing.Algebra.countRingType [in mathcomp.algebra.finalg]
FinRing.Algebra.countType [in mathcomp.algebra.finalg]
+FinRing.Algebra.countZmodType [in mathcomp.algebra.finalg]
FinRing.Algebra.eqType [in mathcomp.algebra.finalg]
FinRing.Algebra.finGroupType [in mathcomp.algebra.finalg]
FinRing.Algebra.finLalgType [in mathcomp.algebra.finalg]
@@ -631,65 +642,77 @@
FinRing.Algebra.finRingType [in mathcomp.algebra.finalg]
FinRing.Algebra.finType [in mathcomp.algebra.finalg]
FinRing.Algebra.finZmodType [in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.Algebra.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finLalgType [in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finLmodType [in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finRingType [in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.Algebra.join_finType [in mathcomp.algebra.finalg]
FinRing.Algebra.lalgType [in mathcomp.algebra.finalg]
FinRing.Algebra.lmodType [in mathcomp.algebra.finalg]
FinRing.Algebra.pack [in mathcomp.algebra.finalg]
FinRing.Algebra.ringType [in mathcomp.algebra.finalg]
FinRing.Algebra.zmodType [in mathcomp.algebra.finalg]
FinRing.ComRing.baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.ComRing.base2 [in mathcomp.algebra.finalg]
FinRing.ComRing.choiceType [in mathcomp.algebra.finalg]
FinRing.ComRing.class [in mathcomp.algebra.finalg]
FinRing.ComRing.comRingType [in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_finRingType [in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_finZmodType [in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_finGroupType [in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.ComRing.comRing_finType [in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRingType [in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_finRingType [in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_finZmodType [in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_finGroupType [in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.ComRing.countComRing_finType [in mathcomp.algebra.finalg]
+FinRing.ComRing.countRingType [in mathcomp.algebra.finalg]
FinRing.ComRing.countType [in mathcomp.algebra.finalg]
+FinRing.ComRing.countZmodType [in mathcomp.algebra.finalg]
FinRing.ComRing.eqType [in mathcomp.algebra.finalg]
FinRing.ComRing.finGroupType [in mathcomp.algebra.finalg]
FinRing.ComRing.finRingType [in mathcomp.algebra.finalg]
FinRing.ComRing.finType [in mathcomp.algebra.finalg]
FinRing.ComRing.finZmodType [in mathcomp.algebra.finalg]
-FinRing.ComRing.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.ComRing.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.ComRing.join_finRingType [in mathcomp.algebra.finalg]
-FinRing.ComRing.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.ComRing.join_finType [in mathcomp.algebra.finalg]
FinRing.ComRing.pack [in mathcomp.algebra.finalg]
FinRing.ComRing.ringType [in mathcomp.algebra.finalg]
FinRing.ComRing.zmodType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.base2 [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.base3 [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.choiceType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.cjoin_finUnitRingType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.class [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.comRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comRing_finUnitRingType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.comUnitRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finUnitRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finComRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finZmodType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finGroupType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.comUnitRing_finType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComRing_finUnitRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finUnitRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finComRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finZmodType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finGroupType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countComUnitRing_finType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countRingType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.countType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countUnitRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countUnitRing_finComRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.countZmodType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.eqType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.fcjoin_finUnitRingType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finComRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.finComRing_finUnitRingType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finGroupType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finRingType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finUnitRingType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.finZmodType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finUnitRingType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finComRingType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finRingType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.join_finType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.pack [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.ringType [in mathcomp.algebra.finalg]
-FinRing.ComUnitRing.ujoin_finComRingType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.unitRingType [in mathcomp.algebra.finalg]
+FinRing.ComUnitRing.unitRing_finComRingType [in mathcomp.algebra.finalg]
FinRing.ComUnitRing.zmodType [in mathcomp.algebra.finalg]
FinRing.DecField.baseFinGroupType [in mathcomp.algebra.finalg]
FinRing.DecField.finComRingType [in mathcomp.algebra.finalg]
@@ -703,14 +726,38 @@
FinRing.DecField.type [in mathcomp.algebra.finalg]
FinRing.DecidableFieldMixin [in mathcomp.algebra.finalg]
FinRing.Field.baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.Field.base2 [in mathcomp.algebra.finalg]
FinRing.Field.choiceType [in mathcomp.algebra.finalg]
FinRing.Field.class [in mathcomp.algebra.finalg]
FinRing.Field.comRingType [in mathcomp.algebra.finalg]
FinRing.Field.comUnitRingType [in mathcomp.algebra.finalg]
+FinRing.Field.countComRingType [in mathcomp.algebra.finalg]
+FinRing.Field.countComUnitRingType [in mathcomp.algebra.finalg]
+FinRing.Field.countFieldType [in mathcomp.algebra.finalg]
+FinRing.Field.countField_finIdomainType [in mathcomp.algebra.finalg]
+FinRing.Field.countField_finComUnitRingType [in mathcomp.algebra.finalg]
+FinRing.Field.countField_finComRingType [in mathcomp.algebra.finalg]
+FinRing.Field.countField_finUnitRingType [in mathcomp.algebra.finalg]
+FinRing.Field.countField_finRingType [in mathcomp.algebra.finalg]
+FinRing.Field.countField_finZmodType [in mathcomp.algebra.finalg]
+FinRing.Field.countField_finGroupType [in mathcomp.algebra.finalg]
+FinRing.Field.countField_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.Field.countField_finType [in mathcomp.algebra.finalg]
+FinRing.Field.countIdomainType [in mathcomp.algebra.finalg]
+FinRing.Field.countRingType [in mathcomp.algebra.finalg]
FinRing.Field.countType [in mathcomp.algebra.finalg]
+FinRing.Field.countUnitRingType [in mathcomp.algebra.finalg]
+FinRing.Field.countZmodType [in mathcomp.algebra.finalg]
FinRing.Field.eqType [in mathcomp.algebra.finalg]
FinRing.Field.fieldType [in mathcomp.algebra.finalg]
+FinRing.Field.field_finIdomainType [in mathcomp.algebra.finalg]
+FinRing.Field.field_finComUnitRingType [in mathcomp.algebra.finalg]
+FinRing.Field.field_finComRingType [in mathcomp.algebra.finalg]
+FinRing.Field.field_finUnitRingType [in mathcomp.algebra.finalg]
+FinRing.Field.field_finRingType [in mathcomp.algebra.finalg]
+FinRing.Field.field_finZmodType [in mathcomp.algebra.finalg]
+FinRing.Field.field_finGroupType [in mathcomp.algebra.finalg]
+FinRing.Field.field_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.Field.field_finType [in mathcomp.algebra.finalg]
FinRing.Field.finComRingType [in mathcomp.algebra.finalg]
FinRing.Field.finComUnitRingType [in mathcomp.algebra.finalg]
FinRing.Field.finGroupType [in mathcomp.algebra.finalg]
@@ -720,15 +767,6 @@
FinRing.Field.finUnitRingType [in mathcomp.algebra.finalg]
FinRing.Field.finZmodType [in mathcomp.algebra.finalg]
FinRing.Field.idomainType [in mathcomp.algebra.finalg]
-FinRing.Field.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.Field.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.Field.join_finIdomainType [in mathcomp.algebra.finalg]
-FinRing.Field.join_finComUnitRingType [in mathcomp.algebra.finalg]
-FinRing.Field.join_finComRingType [in mathcomp.algebra.finalg]
-FinRing.Field.join_finUnitRingType [in mathcomp.algebra.finalg]
-FinRing.Field.join_finRingType [in mathcomp.algebra.finalg]
-FinRing.Field.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.Field.join_finType [in mathcomp.algebra.finalg]
FinRing.Field.pack [in mathcomp.algebra.finalg]
FinRing.Field.ringType [in mathcomp.algebra.finalg]
FinRing.Field.unitRingType [in mathcomp.algebra.finalg]
@@ -736,12 +774,25 @@
FinRing.gen_pack [in mathcomp.algebra.finalg]
FinRing.groupMixin [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.base2 [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.choiceType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.class [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.comRingType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.comUnitRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countComRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countComUnitRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomainType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finComUnitRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finComRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finUnitRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finZmodType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finGroupType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countIdomain_finType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countRingType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.countType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countUnitRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.countZmodType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.eqType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.finComRingType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.finComUnitRingType [in mathcomp.algebra.finalg]
@@ -751,14 +802,14 @@
FinRing.IntegralDomain.finUnitRingType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.finZmodType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.idomainType [in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finComUnitRingType [in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finComRingType [in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finUnitRingType [in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finRingType [in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.IntegralDomain.join_finType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finComUnitRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finComRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finUnitRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finRingType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finZmodType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finGroupType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.IntegralDomain.idomain_finType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.pack [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.ringType [in mathcomp.algebra.finalg]
FinRing.IntegralDomain.unitRingType [in mathcomp.algebra.finalg]
@@ -768,60 +819,74 @@
FinRing.Lalgebra.base3 [in mathcomp.algebra.finalg]
FinRing.Lalgebra.choiceType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.class [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.countRingType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.countType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.countZmodType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.eqType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.finGroupType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.finLmodType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finLmod_finRingType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finLmod_countRingType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.finLmod_ringType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.finRingType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.finType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.finZmodType [in mathcomp.algebra.finalg]
-FinRing.Lalgebra.fljoin_finRingType [in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finRingType [in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finLmodType [in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.Lalgebra.join_finType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.lalgType [in mathcomp.algebra.finalg]
-FinRing.Lalgebra.ljoin_finRingType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finRingType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_countRingType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finLmodType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finZmodType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_countZmodType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finGroupType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_finType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lalg_countType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.lmodType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lmod_finRingType [in mathcomp.algebra.finalg]
+FinRing.Lalgebra.lmod_countRingType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.pack [in mathcomp.algebra.finalg]
FinRing.Lalgebra.ringType [in mathcomp.algebra.finalg]
-FinRing.Lalgebra.rjoin_finLmodType [in mathcomp.algebra.finalg]
FinRing.Lalgebra.zmodType [in mathcomp.algebra.finalg]
FinRing.Lmodule.baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.Lmodule.base2 [in mathcomp.algebra.finalg]
FinRing.Lmodule.choiceType [in mathcomp.algebra.finalg]
FinRing.Lmodule.class [in mathcomp.algebra.finalg]
FinRing.Lmodule.countType [in mathcomp.algebra.finalg]
+FinRing.Lmodule.countZmodType [in mathcomp.algebra.finalg]
FinRing.Lmodule.eqType [in mathcomp.algebra.finalg]
FinRing.Lmodule.finGroupType [in mathcomp.algebra.finalg]
FinRing.Lmodule.finType [in mathcomp.algebra.finalg]
FinRing.Lmodule.finZmodType [in mathcomp.algebra.finalg]
-FinRing.Lmodule.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.Lmodule.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.Lmodule.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.Lmodule.join_finType [in mathcomp.algebra.finalg]
FinRing.Lmodule.lmodType [in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_finZmodType [in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_countZmodType [in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_finGroupType [in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_finType [in mathcomp.algebra.finalg]
+FinRing.Lmodule.lmod_countType [in mathcomp.algebra.finalg]
FinRing.Lmodule.pack [in mathcomp.algebra.finalg]
FinRing.Lmodule.zmodType [in mathcomp.algebra.finalg]
FinRing.Ring.baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.Ring.base2 [in mathcomp.algebra.finalg]
FinRing.Ring.choiceType [in mathcomp.algebra.finalg]
FinRing.Ring.class [in mathcomp.algebra.finalg]
+FinRing.Ring.countRingType [in mathcomp.algebra.finalg]
+FinRing.Ring.countRing_finZmodType [in mathcomp.algebra.finalg]
+FinRing.Ring.countRing_finGroupType [in mathcomp.algebra.finalg]
+FinRing.Ring.countRing_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.Ring.countRing_finType [in mathcomp.algebra.finalg]
FinRing.Ring.countType [in mathcomp.algebra.finalg]
+FinRing.Ring.countZmodType [in mathcomp.algebra.finalg]
FinRing.Ring.eqType [in mathcomp.algebra.finalg]
FinRing.Ring.finGroupType [in mathcomp.algebra.finalg]
FinRing.Ring.finType [in mathcomp.algebra.finalg]
FinRing.Ring.finZmodType [in mathcomp.algebra.finalg]
FinRing.Ring.inv [in mathcomp.algebra.finalg]
FinRing.Ring.is_inv [in mathcomp.algebra.finalg]
-FinRing.Ring.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.Ring.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.Ring.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.Ring.join_finType [in mathcomp.algebra.finalg]
FinRing.Ring.pack [in mathcomp.algebra.finalg]
FinRing.Ring.ringType [in mathcomp.algebra.finalg]
+FinRing.Ring.ring_finZmodType [in mathcomp.algebra.finalg]
+FinRing.Ring.ring_finGroupType [in mathcomp.algebra.finalg]
+FinRing.Ring.ring_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.Ring.ring_finType [in mathcomp.algebra.finalg]
FinRing.Ring.unit [in mathcomp.algebra.finalg]
FinRing.Ring.UnitMixin [in mathcomp.algebra.finalg]
FinRing.Ring.zmodType [in mathcomp.algebra.finalg]
@@ -837,16 +902,23 @@
FinRing.Theory.zmod_abelian [in mathcomp.algebra.finalg]
FinRing.Theory.zmod_mulgC [in mathcomp.algebra.finalg]
FinRing.Theory.zmod1gE [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ajoin_finUnitRingType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.algType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.baseFinGroupType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.base2 [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.base3 [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.choiceType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.class [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countRingType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.countType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRingType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_finAlgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_algType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_finLalgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_lalgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_finLmodType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countUnitRing_lmodType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.countZmodType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.eqType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.fajoin_finUnitRingType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finAlgType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finGroupType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finLalgType [in mathcomp.algebra.finalg]
@@ -854,48 +926,61 @@
FinRing.UnitAlgebra.finRingType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finUnitRingType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_finAlgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_algType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_finLalgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_lalgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_finLmodType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.finUnitRing_lmodType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.finZmodType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.fljoin_finUnitRingType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.fnjoin_finUnitRingType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finAlgType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finLalgType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finLmodType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finUnitRingType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finRingType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.join_finType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.lalgType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ljoin_finUnitRingType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.lmodType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.njoin_finUnitRingType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.pack [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.ringType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ujoin_finAlgType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ujoin_finLalgType [in mathcomp.algebra.finalg]
-FinRing.UnitAlgebra.ujoin_finLmodType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.unitAlgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finAlgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finLalgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finLmodType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finUnitRingType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_countUnitRingType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finRingType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_countRingType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finZmodType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_countZmodType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finGroupType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_finType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitAlg_countType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.unitRingType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitRing_finAlgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitRing_finLalgType [in mathcomp.algebra.finalg]
+FinRing.UnitAlgebra.unitRing_finLmodType [in mathcomp.algebra.finalg]
FinRing.UnitAlgebra.zmodType [in mathcomp.algebra.finalg]
FinRing.UnitRing.baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.UnitRing.base2 [in mathcomp.algebra.finalg]
FinRing.UnitRing.choiceType [in mathcomp.algebra.finalg]
FinRing.UnitRing.class [in mathcomp.algebra.finalg]
+FinRing.UnitRing.countRingType [in mathcomp.algebra.finalg]
FinRing.UnitRing.countType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRingType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_finRingType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_finZmodType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_finGroupType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.countUnitRing_finType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.countZmodType [in mathcomp.algebra.finalg]
FinRing.UnitRing.eqType [in mathcomp.algebra.finalg]
FinRing.UnitRing.finGroupType [in mathcomp.algebra.finalg]
FinRing.UnitRing.finRingType [in mathcomp.algebra.finalg]
FinRing.UnitRing.finType [in mathcomp.algebra.finalg]
FinRing.UnitRing.finZmodType [in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_finRingType [in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_finZmodType [in mathcomp.algebra.finalg]
-FinRing.UnitRing.join_finType [in mathcomp.algebra.finalg]
FinRing.UnitRing.pack [in mathcomp.algebra.finalg]
FinRing.UnitRing.ringType [in mathcomp.algebra.finalg]
FinRing.UnitRing.unitRingType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_finRingType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_finZmodType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_finGroupType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.UnitRing.unitRing_finType [in mathcomp.algebra.finalg]
FinRing.UnitRing.zmodType [in mathcomp.algebra.finalg]
FinRing.unit_act [in mathcomp.algebra.finalg]
FinRing.unit_GroupMixin [in mathcomp.algebra.finalg]
@@ -911,14 +996,18 @@
FinRing.Zmodule.choiceType [in mathcomp.algebra.finalg]
FinRing.Zmodule.class [in mathcomp.algebra.finalg]
FinRing.Zmodule.countType [in mathcomp.algebra.finalg]
+FinRing.Zmodule.countZmodType [in mathcomp.algebra.finalg]
+FinRing.Zmodule.countZmod_finGroupType [in mathcomp.algebra.finalg]
+FinRing.Zmodule.countZmod_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.Zmodule.countZmod_finType [in mathcomp.algebra.finalg]
FinRing.Zmodule.eqType [in mathcomp.algebra.finalg]
FinRing.Zmodule.finGroupType [in mathcomp.algebra.finalg]
FinRing.Zmodule.finType [in mathcomp.algebra.finalg]
-FinRing.Zmodule.join_finGroupType [in mathcomp.algebra.finalg]
-FinRing.Zmodule.join_baseFinGroupType [in mathcomp.algebra.finalg]
-FinRing.Zmodule.join_finType [in mathcomp.algebra.finalg]
FinRing.Zmodule.pack [in mathcomp.algebra.finalg]
FinRing.Zmodule.zmodType [in mathcomp.algebra.finalg]
+FinRing.Zmodule.zmod_finGroupType [in mathcomp.algebra.finalg]
+FinRing.Zmodule.zmod_baseFinGroupType [in mathcomp.algebra.finalg]
+FinRing.Zmodule.zmod_finType [in mathcomp.algebra.finalg]
FinTuple.enum [in mathcomp.ssreflect.tuple]
finv [in mathcomp.ssreflect.fingraph]
fin_pred_sort [in mathcomp.ssreflect.fintype]
@@ -957,13 +1046,13 @@
Frobenius_group [in mathcomp.solvable.frobenius]
Frobenius_group_with_complement [in mathcomp.solvable.frobenius]
fullv [in mathcomp.algebra.vector]
-FunFinfun.finfun [in mathcomp.ssreflect.finfun]
-FunFinfun.fun_of_fin [in mathcomp.ssreflect.finfun]
fun_base [in mathcomp.ssreflect.path]
fun_of_lfun [in mathcomp.algebra.vector]
fun_of_lfun_def [in mathcomp.algebra.vector]
fun_of_matrix [in mathcomp.algebra.matrix]
fun_of_cfun [in mathcomp.character.classfun]
+fun_of_fin [in mathcomp.ssreflect.finfun]
+fun_of_fin_rec [in mathcomp.ssreflect.finfun]
fwith [in mathcomp.ssreflect.eqtype]
F0 [in mathcomp.solvable.burnside_app]
F1 [in mathcomp.solvable.burnside_app]
@@ -1002,7 +1091,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -1034,14 +1123,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -1066,7 +1155,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -1098,7 +1187,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -1130,7 +1219,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -1162,7 +1251,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -1194,7 +1283,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -1226,7 +1315,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -1258,14 +1347,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -1290,7 +1379,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -1322,7 +1411,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -1354,7 +1443,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -1386,14 +1475,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -1418,7 +1507,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
--
cgit v1.2.3