-
Variable Pack :
∀ T,
class_of T → Type → type.
-
Variable Class :
∀ T b,
mixin_of T (
to_choice b)
→ class_of T.
+
Variable Pack :
∀ T,
class_of T → type.
+
Variable Class :
∀ T b,
mixin_of T (
to_choice b)
→ class_of T.
Variable base_class :
∀ bT,
base_of (
base_sort bT).
Definition gen_pack T :=
-
fun bT b &
phant_id (
base_class bT)
b ⇒
-
fun fT m &
phant_id (
Finite.class fT) (
Finite.Class m) ⇒
-
Pack (@
Class T b m)
T.
+
fun bT b &
phant_id (
base_class bT)
b ⇒
+
fun fT m &
phant_id (
Finite.class fT) (
Finite.Class m) ⇒
+
Pack (@
Class T b m).
End Generic.
@@ -116,28 +115,32 @@
Class {
base :
GRing.Zmodule.class_of M;
mixin :
mixin_of M base }.
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Definition pack :=
gen_pack Pack Class GRing.Zmodule.class.
Variable cT :
type.
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
-
-
Definition join_finType := @
Finite.Pack zmodType (
fin_ xclass)
xT.
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group zmodType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition zmod_finType := @
Finite.Pack zmodType (
fin_ xclass).
+
Definition zmod_baseFinGroupType :=
base_group zmodType zmodType finType.
+
Definition zmod_finGroupType :=
fin_group zmod_baseFinGroupType zmodType.
+
Definition countZmod_finType := @
Finite.Pack countZmodType (
fin_ xclass).
+
Definition countZmod_baseFinGroupType :=
+
base_group countZmodType zmodType finType.
+
Definition countZmod_finGroupType :=
+
fin_group countZmod_baseFinGroupType zmodType.
End ClassDef.
@@ -145,6 +148,7 @@
Module Exports.
Coercion base : class_of >-> GRing.Zmodule.class_of.
+
Coercion base2 : class_of >-> CountRing.Zmodule.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
@@ -155,24 +159,29 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
-
Coercion zmodType : type >-> GRing.Zmodule.type.
-
Canonical zmodType.
-
Canonical join_finType.
-
Notation finZmodType :=
type.
-
Notation "[ 'finZmodType' 'of' T ]" := (
do_pack pack T)
- (
at level 0,
format "[ 'finZmodType' 'of' T ]") :
form_scope.
Coercion baseFinGroupType : type >-> FinGroup.base_type.
Canonical baseFinGroupType.
Coercion finGroupType : type >-> FinGroup.type.
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
-
Notation "[ 'baseFinGroupType' 'of' R 'for' +%R ]" :=
+
Coercion zmodType : type >-> GRing.Zmodule.type.
+
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
+
Canonical zmod_finType.
+
Canonical zmod_baseFinGroupType.
+
Canonical zmod_finGroupType.
+
Canonical countZmod_finType.
+
Canonical countZmod_baseFinGroupType.
+
Canonical countZmod_finGroupType.
+
Notation finZmodType :=
type.
+
Notation "[ 'finZmodType' 'of' T ]" := (
do_pack pack T)
+ (
at level 0,
format "[ 'finZmodType' 'of' T ]") :
form_scope.
+
Notation "[ 'baseFinGroupType' 'of' R 'for' +%R ]" :=
(
BaseFinGroupType R (
groupMixin _))
(
at level 0,
format "[ 'baseFinGroupType' 'of' R 'for' +%R ]")
:
form_scope.
-
Notation "[ 'finGroupType' 'of' R 'for' +%R ]" :=
- (@
FinGroup.clone R _ (
finGroupType _)
id _ id)
+
Notation "[ 'finGroupType' 'of' R 'for' +%R ]" :=
+ (@
FinGroup.clone R _ (
finGroupType _)
id _ id)
(
at level 0,
format "[ 'finGroupType' 'of' R 'for' +%R ]") :
form_scope.
End Exports.
@@ -188,12 +197,12 @@
Implicit Types x y :
U.
-
Lemma zmod1gE : 1%
g = 0
:> U.
-
Lemma zmodVgE x :
x^-1%
g = - x.
-
Lemma zmodMgE x y : (
x × y)%
g = x + y.
-
Lemma zmodXgE n x : (
x ^+ n)%
g = x *+ n.
+
Lemma zmod1gE : 1%
g = 0
:> U.
+
Lemma zmodVgE x :
x^-1%
g = - x.
+
Lemma zmodMgE x y : (
x × y)%
g = x + y.
+
Lemma zmodXgE n x : (
x ^+ n)%
g = x *+ n.
Lemma zmod_mulgC x y :
commute x y.
-
Lemma zmod_abelian (
A :
{set U}) :
abelian A.
+
Lemma zmod_abelian (
A :
{set U}) :
abelian A.
End AdditiveGroup.
@@ -207,32 +216,39 @@
Record class_of R :=
Class {
base :
GRing.Ring.class_of R;
mixin :
mixin_of R base }.
-
Definition base2 R (
c :
class_of R) :=
Zmodule.Class (
mixin c).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Definition pack :=
gen_pack Pack Class GRing.Ring.class.
Variable cT :
type.
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
cT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass cT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition join_finType := @
Finite.Pack ringType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack ringType xclass xT.
-
-
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition countRingType := @
CountRing.Ring.Pack cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group ringType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition ring_finType := @
Finite.Pack ringType (
fin_ xclass).
+
Definition ring_baseFinGroupType :=
base_group ringType zmodType finType.
+
Definition ring_finGroupType :=
fin_group ring_baseFinGroupType zmodType.
+
Definition ring_finZmodType := @
Zmodule.Pack ringType xclass.
+
Definition countRing_finType := @
Finite.Pack countRingType (
fin_ xclass).
+
Definition countRing_baseFinGroupType :=
+
base_group countRingType zmodType finType.
+
Definition countRing_finGroupType :=
+
fin_group countRing_baseFinGroupType zmodType.
+
Definition countRing_finZmodType := @
Zmodule.Pack countRingType xclass.
End ClassDef.
@@ -240,7 +256,8 @@
Module Import Exports.
Coercion base : class_of >-> GRing.Ring.class_of.
-
Coercion base2 : class_of >-> Zmodule.class_of.
+
Coercion base2 : class_of >-> CountRing.Ring.class_of.
+
Coercion base3 : class_of >-> Zmodule.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
@@ -250,21 +267,31 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
+
Coercion countRingType : type >-> CountRing.Ring.type.
+
Canonical countRingType.
+
Canonical ring_finType.
+
Canonical ring_baseFinGroupType.
+
Canonical ring_finGroupType.
+
Canonical ring_finZmodType.
+
Canonical countRing_finType.
+
Canonical countRing_baseFinGroupType.
+
Canonical countRing_finGroupType.
+
Canonical countRing_finZmodType.
Notation finRingType :=
type.
-
Notation "[ 'finRingType' 'of' T ]" := (
do_pack pack T)
+
Notation "[ 'finRingType' 'of' T ]" := (
do_pack pack T)
(
at level 0,
format "[ 'finRingType' 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -274,21 +301,21 @@
Variable R :
finRingType.
-
Definition is_inv (
x y :
R) :=
(x × y == 1
) && (y × x == 1
).
-
Definition unit :=
[qualify a x : R | [∃ y, is_inv x y]].
-
Definition inv x :=
odflt x (
pick (
is_inv x)).
+
Definition is_inv (
x y :
R) :=
(x × y == 1
) && (y × x == 1
).
+
Definition unit :=
[qualify a x : R | [∃ y, is_inv x y]].
+
Definition inv x :=
odflt x (
pick (
is_inv x)).
-
Lemma mulVr :
{in unit, left_inverse 1
inv *%R}.
+
Lemma mulVr :
{in unit, left_inverse 1
inv *%R}.
-
Lemma mulrV :
{in unit, right_inverse 1
inv *%R}.
+
Lemma mulrV :
{in unit, right_inverse 1
inv *%R}.
-
Lemma intro_unit x y :
y × x = 1
∧ x × y = 1
→ x \is a unit.
+
Lemma intro_unit x y :
y × x = 1
∧ x × y = 1
→ x \is a unit.
-
Lemma invr_out :
{in [predC unit], inv =1 id}.
+
Lemma invr_out :
{in [predC unit], inv =1 id}.
Definition UnitMixin :=
GRing.UnitRing.Mixin mulVr mulrV intro_unit invr_out.
@@ -309,35 +336,44 @@
Record class_of R :=
Class {
base :
GRing.ComRing.class_of R;
mixin :
mixin_of R base }.
-
Definition base2 R (
c :
class_of R) :=
Ring.Class (
mixin c).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Definition pack :=
gen_pack Pack Class GRing.ComRing.class.
Variable cT :
type.
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition finRingType := @
Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition join_finType := @
Finite.Pack comRingType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack comRingType xclass xT.
-
Definition join_finRingType := @
Ring.Pack comRingType xclass xT.
-
-
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition countRingType := @
CountRing.Ring.Pack cT xclass.
+
Definition finRingType := @
Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition countComRingType := @
CountRing.ComRing.Pack cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group comRingType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition comRing_finType := @
Finite.Pack comRingType (
fin_ xclass).
+
Definition comRing_baseFinGroupType :=
base_group comRingType zmodType finType.
+
Definition comRing_finGroupType :=
fin_group comRing_baseFinGroupType zmodType.
+
Definition comRing_finZmodType := @
Zmodule.Pack comRingType xclass.
+
Definition comRing_finRingType := @
Ring.Pack comRingType xclass.
+
Definition countComRing_finType := @
Finite.Pack countComRingType (
fin_ xclass).
+
Definition countComRing_baseFinGroupType :=
+
base_group countComRingType zmodType finType.
+
Definition countComRing_finGroupType :=
+
fin_group countComRing_baseFinGroupType zmodType.
+
Definition countComRing_finZmodType := @
Zmodule.Pack countComRingType xclass.
+
Definition countComRing_finRingType := @
Ring.Pack countComRingType xclass.
End ClassDef.
@@ -345,7 +381,8 @@
Module Exports.
Coercion base : class_of >-> GRing.ComRing.class_of.
-
Coercion base2 : class_of >-> Ring.class_of.
+
Coercion base2 : class_of >-> CountRing.ComRing.class_of.
+
Coercion base3 : class_of >-> Ring.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
@@ -355,26 +392,39 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
+
Coercion countRingType : type >-> CountRing.Ring.type.
+
Canonical countRingType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
-
Canonical join_finRingType.
+
Coercion countComRingType : type >-> CountRing.ComRing.type.
+
Canonical countComRingType.
+
Canonical comRing_finType.
+
Canonical comRing_baseFinGroupType.
+
Canonical comRing_finGroupType.
+
Canonical comRing_finZmodType.
+
Canonical comRing_finRingType.
+
Canonical countComRing_finType.
+
Canonical countComRing_baseFinGroupType.
+
Canonical countComRing_finGroupType.
+
Canonical countComRing_finZmodType.
+
Canonical countComRing_finRingType.
Notation finComRingType :=
FinRing.ComRing.type.
-
Notation "[ 'finComRingType' 'of' T ]" := (
do_pack pack T)
+
Notation "[ 'finComRingType' 'of' T ]" := (
do_pack pack T)
(
at level 0,
format "[ 'finComRingType' 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -390,37 +440,47 @@
Record class_of R :=
Class {
base :
GRing.UnitRing.class_of R;
mixin :
mixin_of R base }.
-
Definition base2 R (
c :
class_of R) :=
Ring.Class (
mixin c).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Definition pack :=
gen_pack Pack Class GRing.UnitRing.class.
Variable cT :
type.
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition finRingType := @
Ring.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
-
-
Definition join_finType := @
Finite.Pack unitRingType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack unitRingType xclass xT.
-
Definition join_finRingType := @
Ring.Pack unitRingType xclass xT.
-
-
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition countRingType := @
CountRing.Ring.Pack cT xclass.
+
Definition finRingType := @
Ring.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition countUnitRingType := @
CountRing.UnitRing.Pack cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group unitRingType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition unitRing_finType := @
Finite.Pack unitRingType (
fin_ xclass).
+
Definition unitRing_baseFinGroupType :=
+
base_group unitRingType zmodType finType.
+
Definition unitRing_finGroupType :=
+
fin_group unitRing_baseFinGroupType zmodType.
+
Definition unitRing_finZmodType := @
Zmodule.Pack unitRingType xclass.
+
Definition unitRing_finRingType := @
Ring.Pack unitRingType xclass.
+
Definition countUnitRing_finType :=
+ @
Finite.Pack countUnitRingType (
fin_ xclass).
+
Definition countUnitRing_baseFinGroupType :=
+
base_group countUnitRingType zmodType finType.
+
Definition countUnitRing_finGroupType :=
+
fin_group countUnitRing_baseFinGroupType zmodType.
+
Definition countUnitRing_finZmodType := @
Zmodule.Pack countUnitRingType xclass.
+
Definition countUnitRing_finRingType := @
Ring.Pack countUnitRingType xclass.
End ClassDef.
@@ -428,7 +488,8 @@
Module Exports.
Coercion base : class_of >-> GRing.UnitRing.class_of.
-
Coercion base2 : class_of >-> Ring.class_of.
+
Coercion base2 : class_of >-> CountRing.UnitRing.class_of.
+
Coercion base3 : class_of >-> Ring.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
@@ -438,26 +499,39 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
+
Coercion countRingType : type >-> CountRing.Ring.type.
+
Canonical countRingType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
-
Canonical join_finRingType.
+
Coercion countUnitRingType : type >-> CountRing.UnitRing.type.
+
Canonical countUnitRingType.
+
Canonical unitRing_finType.
+
Canonical unitRing_baseFinGroupType.
+
Canonical unitRing_finGroupType.
+
Canonical unitRing_finZmodType.
+
Canonical unitRing_finRingType.
+
Canonical countUnitRing_finType.
+
Canonical countUnitRing_baseFinGroupType.
+
Canonical countUnitRing_finGroupType.
+
Canonical countUnitRing_finZmodType.
+
Canonical countUnitRing_finRingType.
Notation finUnitRingType :=
FinRing.UnitRing.type.
-
Notation "[ 'finUnitRingType' 'of' T ]" := (
do_pack pack T)
+
Notation "[ 'finUnitRingType' 'of' T ]" := (
do_pack pack T)
(
at level 0,
format "[ 'finUnitRingType' 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -471,35 +545,35 @@
Variable R :
finUnitRingType.
-
Inductive unit_of (
phR :
phant R) :=
Unit (
x :
R)
of x \is a GRing.unit.
+
Inductive unit_of (
phR :
phant R) :=
Unit (
x :
R)
of x \is a GRing.unit.
-
Let phR :=
Phant R.
+
Let phR :=
Phant R.
Implicit Types u v :
uT.
Definition uval u :=
let:
Unit x _ :=
u in x.
-
Canonical unit_subType :=
[subType for uval].
-
Definition unit_eqMixin :=
Eval hnf in [eqMixin of uT by <:].
+
Canonical unit_subType :=
[subType for uval].
+
Definition unit_eqMixin :=
Eval hnf in [eqMixin of uT by <:].
Canonical unit_eqType :=
Eval hnf in EqType uT unit_eqMixin.
-
Definition unit_choiceMixin :=
[choiceMixin of uT by <:].
+
Definition unit_choiceMixin :=
[choiceMixin of uT by <:].
Canonical unit_choiceType :=
Eval hnf in ChoiceType uT unit_choiceMixin.
-
Definition unit_countMixin :=
[countMixin of uT by <:].
+
Definition unit_countMixin :=
[countMixin of uT by <:].
Canonical unit_countType :=
Eval hnf in CountType uT unit_countMixin.
-
Canonical unit_subCountType :=
Eval hnf in [subCountType of uT].
-
Definition unit_finMixin :=
[finMixin of uT by <:].
+
Canonical unit_subCountType :=
Eval hnf in [subCountType of uT].
+
Definition unit_finMixin :=
[finMixin of uT by <:].
Canonical unit_finType :=
Eval hnf in FinType uT unit_finMixin.
-
Canonical unit_subFinType :=
Eval hnf in [subFinType of uT].
+
Canonical unit_subFinType :=
Eval hnf in [subFinType of uT].
Definition unit1 :=
Unit phR (@
GRing.unitr1 _).
-
Lemma unit_inv_proof u :
(val u)^-1 \is a GRing.unit.
+
Lemma unit_inv_proof u :
(val u)^-1 \is a GRing.unit.
Definition unit_inv u :=
Unit phR (
unit_inv_proof u).
-
Lemma unit_mul_proof u v :
val u × val v \is a GRing.unit.
+
Lemma unit_mul_proof u v :
val u × val v \is a GRing.unit.
Definition unit_mul u v :=
Unit phR (
unit_mul_proof u v).
-
Lemma unit_muluA :
associative unit_mul.
-
Lemma unit_mul1u :
left_id unit1 unit_mul.
-
Lemma unit_mulVu :
left_inverse unit1 unit_inv unit_mul.
+
Lemma unit_muluA :
associative unit_mul.
+
Lemma unit_mul1u :
left_id unit1 unit_mul.
+
Lemma unit_mulVu :
left_inverse unit1 unit_inv unit_mul.
Definition unit_GroupMixin :=
FinGroup.Mixin unit_muluA unit_mul1u unit_mulVu.
@@ -508,14 +582,14 @@
Canonical unit_finGroupType :=
Eval hnf in FinGroupType unit_mulVu.
-
Lemma val_unit1 :
val (1%
g : uT)
= 1.
-
Lemma val_unitM x y :
val (
x × y : uT)%
g = val x × val y.
-
Lemma val_unitV x :
val (
x^-1 : uT)%
g = (val x)^-1.
-
Lemma val_unitX n x :
val (
x ^+ n : uT)%
g = val x ^+ n.
+
Lemma val_unit1 :
val (1%
g : uT)
= 1.
+
Lemma val_unitM x y :
val (
x × y : uT)%
g = val x × val y.
+
Lemma val_unitV x :
val (
x^-1 : uT)%
g = (val x)^-1.
+
Lemma val_unitX n x :
val (
x ^+ n : uT)%
g = val x ^+ n.
-
Definition unit_act x u :=
x × val u.
-
Lemma unit_actE x u :
unit_act x u = x × val u.
+
Definition unit_act x u :=
x × val u.
+
Lemma unit_actE x u :
unit_act x u = x × val u.
Canonical unit_action :=
@@ -542,7 +616,7 @@
End UnitsGroupExports.
-
Notation unit R Ux := (
Unit (
Phant R)
Ux).
+
Notation unit R Ux := (
Unit (
Phant R)
Ux).
Module ComUnitRing.
@@ -553,47 +627,68 @@
Record class_of R :=
Class {
base :
GRing.ComUnitRing.class_of R;
mixin :
mixin_of R base }.
-
Definition base2 R (
c :
class_of R) :=
ComRing.Class (
mixin c).
-
Definition base3 R (
c :
class_of R) := @
UnitRing.Class R (
base c) (
mixin c).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Definition pack :=
gen_pack Pack Class GRing.ComUnitRing.class.
Variable cT :
type.
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition finRingType := @
Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition finComRingType := @
ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition finUnitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
-
-
Definition join_finType := @
Finite.Pack comUnitRingType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack comUnitRingType xclass xT.
-
Definition join_finRingType := @
Ring.Pack comUnitRingType xclass xT.
-
Definition join_finComRingType := @
ComRing.Pack comUnitRingType xclass xT.
-
Definition join_finUnitRingType := @
UnitRing.Pack comUnitRingType xclass xT.
-
Definition ujoin_finComRingType := @
ComRing.Pack unitRingType xclass xT.
-
Definition cjoin_finUnitRingType := @
UnitRing.Pack comRingType xclass xT.
-
Definition fcjoin_finUnitRingType := @
UnitRing.Pack finComRingType xclass xT.
-
-
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition countRingType := @
CountRing.Ring.Pack cT xclass.
+
Definition finRingType := @
Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition countComRingType := @
CountRing.ComRing.Pack cT xclass.
+
Definition finComRingType := @
ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition countUnitRingType := @
CountRing.UnitRing.Pack cT xclass.
+
Definition finUnitRingType := @
UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition countComUnitRingType := @
CountRing.ComUnitRing.Pack cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group comUnitRingType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition comUnitRing_finType := @
Finite.Pack comUnitRingType (
fin_ xclass).
+
Definition comUnitRing_baseFinGroupType :=
+
base_group comUnitRingType zmodType finType.
+
Definition comUnitRing_finGroupType :=
+
fin_group comUnitRing_baseFinGroupType zmodType.
+
Definition comUnitRing_finZmodType := @
Zmodule.Pack comUnitRingType xclass.
+
Definition comUnitRing_finRingType := @
Ring.Pack comUnitRingType xclass.
+
Definition comUnitRing_finComRingType := @
ComRing.Pack comUnitRingType xclass.
+
Definition comUnitRing_finUnitRingType := @
UnitRing.Pack comUnitRingType xclass.
+
Definition countComUnitRing_finType :=
+ @
Finite.Pack countComUnitRingType (
fin_ xclass).
+
Definition countComUnitRing_baseFinGroupType :=
+
base_group countComUnitRingType zmodType finType.
+
Definition countComUnitRing_finGroupType :=
+
fin_group countComUnitRing_baseFinGroupType zmodType.
+
Definition countComUnitRing_finZmodType :=
+ @
Zmodule.Pack countComUnitRingType xclass.
+
Definition countComUnitRing_finRingType :=
+ @
Ring.Pack countComUnitRingType xclass.
+
Definition countComUnitRing_finComRingType :=
+ @
ComRing.Pack countComUnitRingType xclass.
+
Definition countComUnitRing_finUnitRingType :=
+ @
UnitRing.Pack countComUnitRingType xclass.
+
Definition unitRing_finComRingType := @
ComRing.Pack unitRingType xclass.
+
Definition countUnitRing_finComRingType :=
+ @
ComRing.Pack countUnitRingType xclass.
+
Definition comRing_finUnitRingType := @
UnitRing.Pack comRingType xclass.
+
Definition countComRing_finUnitRingType :=
+ @
UnitRing.Pack countComRingType xclass.
+
Definition finComRing_finUnitRingType := @
UnitRing.Pack finComRingType xclass.
End ClassDef.
@@ -601,8 +696,9 @@
Module Exports.
Coercion base : class_of >-> GRing.ComUnitRing.class_of.
-
Coercion base2 : class_of >-> ComRing.class_of.
-
Coercion base3 : class_of >-> UnitRing.class_of.
+
Coercion base2 : class_of >-> CountRing.ComUnitRing.class_of.
+
Coercion base3 : class_of >-> ComRing.class_of.
+
Coercion base4 : class_of >-> UnitRing.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
@@ -612,39 +708,60 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
+
Coercion countRingType : type >-> CountRing.Ring.type.
+
Canonical countRingType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
+
Coercion countComRingType : type >-> CountRing.ComRing.type.
+
Canonical countComRingType.
Coercion finComRingType : type >-> ComRing.type.
Canonical finComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
+
Coercion countUnitRingType : type >-> CountRing.UnitRing.type.
+
Canonical countUnitRingType.
Coercion finUnitRingType : type >-> UnitRing.type.
Canonical finUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
-
Canonical join_finRingType.
-
Canonical join_finComRingType.
-
Canonical join_finUnitRingType.
-
Canonical ujoin_finComRingType.
-
Canonical cjoin_finUnitRingType.
-
Canonical fcjoin_finUnitRingType.
+
Coercion countComUnitRingType : type >-> CountRing.ComUnitRing.type.
+
Canonical countComUnitRingType.
+
Canonical comUnitRing_finType.
+
Canonical comUnitRing_baseFinGroupType.
+
Canonical comUnitRing_finGroupType.
+
Canonical comUnitRing_finZmodType.
+
Canonical comUnitRing_finRingType.
+
Canonical comUnitRing_finComRingType.
+
Canonical comUnitRing_finUnitRingType.
+
Canonical countComUnitRing_finType.
+
Canonical countComUnitRing_baseFinGroupType.
+
Canonical countComUnitRing_finGroupType.
+
Canonical countComUnitRing_finZmodType.
+
Canonical countComUnitRing_finRingType.
+
Canonical countComUnitRing_finComRingType.
+
Canonical countComUnitRing_finUnitRingType.
+
Canonical unitRing_finComRingType.
+
Canonical countUnitRing_finComRingType.
+
Canonical comRing_finUnitRingType.
+
Canonical countComRing_finUnitRingType.
+
Canonical finComRing_finUnitRingType.
Notation finComUnitRingType :=
FinRing.ComUnitRing.type.
-
Notation "[ 'finComUnitRingType' 'of' T ]" := (
do_pack pack T)
+
Notation "[ 'finComUnitRingType' 'of' T ]" := (
do_pack pack T)
(
at level 0,
format "[ 'finComUnitRingType' 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -660,46 +777,61 @@
Record class_of R :=
Class {
base :
GRing.IntegralDomain.class_of R;
mixin :
mixin_of R base }.
-
Definition base2 R (
c :
class_of R) :=
ComUnitRing.Class (
mixin c).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Definition pack :=
gen_pack Pack Class GRing.IntegralDomain.class.
Variable cT :
type.
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition finRingType := @
Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition finComRingType := @
ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition finUnitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
Definition finComUnitRingType := @
ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass xT.
-
-
-
Definition join_finType := @
Finite.Pack idomainType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack idomainType xclass xT.
-
Definition join_finRingType := @
Ring.Pack idomainType xclass xT.
-
Definition join_finUnitRingType := @
UnitRing.Pack idomainType xclass xT.
-
Definition join_finComRingType := @
ComRing.Pack idomainType xclass xT.
-
Definition join_finComUnitRingType := @
ComUnitRing.Pack idomainType xclass xT.
-
-
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition countRingType := @
CountRing.Ring.Pack cT xclass.
+
Definition finRingType := @
Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition countComRingType := @
CountRing.ComRing.Pack cT xclass.
+
Definition finComRingType := @
ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition countUnitRingType := @
CountRing.UnitRing.Pack cT xclass.
+
Definition finUnitRingType := @
UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition countComUnitRingType := @
CountRing.ComUnitRing.Pack cT xclass.
+
Definition finComUnitRingType := @
ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass.
+
Definition countIdomainType := @
CountRing.IntegralDomain.Pack cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group idomainType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition idomain_finType := @
Finite.Pack idomainType (
fin_ xclass).
+
Definition idomain_baseFinGroupType :=
base_group idomainType zmodType finType.
+
Definition idomain_finGroupType :=
fin_group idomain_baseFinGroupType zmodType.
+
Definition idomain_finZmodType := @
Zmodule.Pack idomainType xclass.
+
Definition idomain_finRingType := @
Ring.Pack idomainType xclass.
+
Definition idomain_finUnitRingType := @
UnitRing.Pack idomainType xclass.
+
Definition idomain_finComRingType := @
ComRing.Pack idomainType xclass.
+
Definition idomain_finComUnitRingType := @
ComUnitRing.Pack idomainType xclass.
+
Definition countIdomain_finType := @
Finite.Pack countIdomainType (
fin_ xclass).
+
Definition countIdomain_baseFinGroupType :=
+
base_group countIdomainType zmodType finType.
+
Definition countIdomain_finGroupType :=
+
fin_group countIdomain_baseFinGroupType zmodType.
+
Definition countIdomain_finZmodType := @
Zmodule.Pack countIdomainType xclass.
+
Definition countIdomain_finRingType := @
Ring.Pack countIdomainType xclass.
+
Definition countIdomain_finUnitRingType :=
+ @
UnitRing.Pack countIdomainType xclass.
+
Definition countIdomain_finComRingType := @
ComRing.Pack countIdomainType xclass.
+
Definition countIdomain_finComUnitRingType :=
+ @
ComUnitRing.Pack countIdomainType xclass.
End ClassDef.
@@ -707,7 +839,8 @@
Module Exports.
Coercion base : class_of >-> GRing.IntegralDomain.class_of.
-
Coercion base2 : class_of >-> ComUnitRing.class_of.
+
Coercion base2 : class_of >-> CountRing.IntegralDomain.class_of.
+
Coercion base3 : class_of >-> ComUnitRing.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
@@ -717,41 +850,63 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
+
Coercion countRingType : type >-> CountRing.Ring.type.
+
Canonical countRingType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
+
Coercion countComRingType : type >-> CountRing.ComRing.type.
+
Canonical countComRingType.
Coercion finComRingType : type >-> ComRing.type.
Canonical finComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
+
Coercion countUnitRingType : type >-> CountRing.UnitRing.type.
+
Canonical countUnitRingType.
Coercion finUnitRingType : type >-> UnitRing.type.
Canonical finUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
+
Coercion countComUnitRingType : type >-> CountRing.ComUnitRing.type.
+
Canonical countComUnitRingType.
Coercion finComUnitRingType : type >-> ComUnitRing.type.
Canonical finComUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
-
Canonical join_finRingType.
-
Canonical join_finComRingType.
-
Canonical join_finUnitRingType.
-
Canonical join_finComUnitRingType.
+
Coercion countIdomainType : type >-> CountRing.IntegralDomain.type.
+
Canonical countIdomainType.
+
Canonical idomain_finType.
+
Canonical idomain_baseFinGroupType.
+
Canonical idomain_finGroupType.
+
Canonical idomain_finZmodType.
+
Canonical idomain_finRingType.
+
Canonical idomain_finUnitRingType.
+
Canonical idomain_finComRingType.
+
Canonical idomain_finComUnitRingType.
+
Canonical countIdomain_finType.
+
Canonical countIdomain_baseFinGroupType.
+
Canonical countIdomain_finGroupType.
+
Canonical countIdomain_finZmodType.
+
Canonical countIdomain_finRingType.
+
Canonical countIdomain_finUnitRingType.
+
Canonical countIdomain_finComRingType.
+
Canonical countIdomain_finComUnitRingType.
Notation finIdomainType :=
FinRing.IntegralDomain.type.
-
Notation "[ 'finIdomainType' 'of' T ]" := (
do_pack pack T)
+
Notation "[ 'finIdomainType' 'of' T ]" := (
do_pack pack T)
(
at level 0,
format "[ 'finIdomainType' 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -767,49 +922,66 @@
Record class_of R :=
Class {
base :
GRing.Field.class_of R;
mixin :
mixin_of R base }.
-
Definition base2 R (
c :
class_of R) :=
IntegralDomain.Class (
mixin c).
-
Structure type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :=
Pack {
sort;
_ :
class_of sort}.
Definition pack :=
gen_pack Pack Class GRing.Field.class.
Variable cT :
type.
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition finRingType := @
Ring.Pack cT xclass xT.
-
Definition comRingType := @
GRing.ComRing.Pack cT xclass xT.
-
Definition finComRingType := @
ComRing.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition finUnitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass xT.
-
Definition finComUnitRingType := @
ComUnitRing.Pack cT xclass xT.
-
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass xT.
-
Definition finIdomainType := @
IntegralDomain.Pack cT xclass xT.
-
Definition fieldType := @
GRing.Field.Pack cT xclass xT.
-
-
-
Definition join_finType := @
Finite.Pack fieldType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack fieldType xclass xT.
-
Definition join_finRingType := @
Ring.Pack fieldType xclass xT.
-
Definition join_finUnitRingType := @
UnitRing.Pack fieldType xclass xT.
-
Definition join_finComRingType := @
ComRing.Pack fieldType xclass xT.
-
Definition join_finComUnitRingType := @
ComUnitRing.Pack fieldType xclass xT.
-
Definition join_finIdomainType := @
IntegralDomain.Pack fieldType xclass xT.
-
-
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition countRingType := @
CountRing.Ring.Pack cT xclass.
+
Definition finRingType := @
Ring.Pack cT xclass.
+
Definition comRingType := @
GRing.ComRing.Pack cT xclass.
+
Definition countComRingType := @
CountRing.ComRing.Pack cT xclass.
+
Definition finComRingType := @
ComRing.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition countUnitRingType := @
CountRing.UnitRing.Pack cT xclass.
+
Definition finUnitRingType := @
UnitRing.Pack cT xclass.
+
Definition comUnitRingType := @
GRing.ComUnitRing.Pack cT xclass.
+
Definition countComUnitRingType := @
CountRing.ComUnitRing.Pack cT xclass.
+
Definition finComUnitRingType := @
ComUnitRing.Pack cT xclass.
+
Definition idomainType := @
GRing.IntegralDomain.Pack cT xclass.
+
Definition countIdomainType := @
CountRing.IntegralDomain.Pack cT xclass.
+
Definition finIdomainType := @
IntegralDomain.Pack cT xclass.
+
Definition fieldType := @
GRing.Field.Pack cT xclass.
+
Definition countFieldType := @
CountRing.Field.Pack cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group fieldType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition field_finType := @
Finite.Pack fieldType (
fin_ xclass).
+
Definition field_baseFinGroupType :=
base_group fieldType zmodType finType.
+
Definition field_finGroupType :=
fin_group field_baseFinGroupType zmodType.
+
Definition field_finZmodType := @
Zmodule.Pack fieldType xclass.
+
Definition field_finRingType := @
Ring.Pack fieldType xclass.
+
Definition field_finUnitRingType := @
UnitRing.Pack fieldType xclass.
+
Definition field_finComRingType := @
ComRing.Pack fieldType xclass.
+
Definition field_finComUnitRingType := @
ComUnitRing.Pack fieldType xclass.
+
Definition field_finIdomainType := @
IntegralDomain.Pack fieldType xclass.
+
Definition countField_finType := @
Finite.Pack countFieldType (
fin_ xclass).
+
Definition countField_baseFinGroupType :=
+
base_group countFieldType zmodType finType.
+
Definition countField_finGroupType :=
+
fin_group countField_baseFinGroupType zmodType.
+
Definition countField_finZmodType := @
Zmodule.Pack countFieldType xclass.
+
Definition countField_finRingType := @
Ring.Pack countFieldType xclass.
+
Definition countField_finUnitRingType := @
UnitRing.Pack countFieldType xclass.
+
Definition countField_finComRingType := @
ComRing.Pack countFieldType xclass.
+
Definition countField_finComUnitRingType :=
+ @
ComUnitRing.Pack countFieldType xclass.
+
Definition countField_finIdomainType :=
+ @
IntegralDomain.Pack countFieldType xclass.
End ClassDef.
@@ -817,7 +989,8 @@
Module Exports.
Coercion base : class_of >-> GRing.Field.class_of.
-
Coercion base2 : class_of >-> IntegralDomain.class_of.
+
Coercion base2 : class_of >-> CountRing.Field.class_of.
+
Coercion base3 : class_of >-> IntegralDomain.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
@@ -827,46 +1000,71 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
+
Coercion countRingType : type >-> CountRing.Ring.type.
+
Canonical countRingType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
+
Coercion countComRingType : type >-> CountRing.ComRing.type.
+
Canonical countComRingType.
Coercion finComRingType : type >-> ComRing.type.
Canonical finComRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
+
Coercion countUnitRingType : type >-> CountRing.UnitRing.type.
+
Canonical countUnitRingType.
Coercion finUnitRingType : type >-> UnitRing.type.
Canonical finUnitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
+
Coercion countComUnitRingType : type >-> CountRing.ComUnitRing.type.
+
Canonical countComUnitRingType.
Coercion finComUnitRingType : type >-> ComUnitRing.type.
Canonical finComUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
+
Coercion countIdomainType : type >-> CountRing.IntegralDomain.type.
+
Canonical countIdomainType.
Coercion finIdomainType : type >-> IntegralDomain.type.
Canonical finIdomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
-
Canonical join_finRingType.
-
Canonical join_finComRingType.
-
Canonical join_finUnitRingType.
-
Canonical join_finComUnitRingType.
-
Canonical join_finIdomainType.
+
Coercion countFieldType : type >-> CountRing.Field.type.
+
Canonical countFieldType.
+
Canonical field_finType.
+
Canonical field_baseFinGroupType.
+
Canonical field_finGroupType.
+
Canonical field_finZmodType.
+
Canonical field_finRingType.
+
Canonical field_finUnitRingType.
+
Canonical field_finComRingType.
+
Canonical field_finComUnitRingType.
+
Canonical field_finIdomainType.
+
Canonical countField_finType.
+
Canonical countField_baseFinGroupType.
+
Canonical countField_finGroupType.
+
Canonical countField_finZmodType.
+
Canonical countField_finRingType.
+
Canonical countField_finUnitRingType.
+
Canonical countField_finComRingType.
+
Canonical countField_finComUnitRingType.
+
Canonical countField_finIdomainType.
Notation finFieldType :=
FinRing.Field.type.
-
Notation "[ 'finFieldType' 'of' T ]" := (
do_pack pack T)
+
Notation "[ 'finFieldType' 'of' T ]" := (
do_pack pack T)
(
at level 0,
format "[ 'finFieldType' 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -883,14 +1081,14 @@
Fixpoint sat e f :=
match f with
|
GRing.Bool b ⇒
b
- |
t1 == t2 ⇒ (
GRing.eval e t1 == GRing.eval e t2)%
bool
- |
GRing.Unit t ⇒
GRing.eval e t \is a GRing.unit
- |
f1 ∧ f2 ⇒
sat e f1 && sat e f2
- |
f1 ∨ f2 ⇒
sat e f1 || sat e f2
- |
f1 ==> f2 ⇒ (
sat e f1 ==> sat e f2)%
bool
- |
¬ f1 ⇒
~~ sat e f1
- | (
'∃ 'X_k, f1) ⇒
[∃ x : F, sat (
set_nth 0%
R e k x)
f1]
- | (
'∀ 'X_k, f1) ⇒
[∀ x : F, sat (
set_nth 0%
R e k x)
f1]
+ |
t1 == t2 ⇒ (
GRing.eval e t1 == GRing.eval e t2)%
bool
+ |
GRing.Unit t ⇒
GRing.eval e t \is a GRing.unit
+ |
f1 ∧ f2 ⇒
sat e f1 && sat e f2
+ |
f1 ∨ f2 ⇒
sat e f1 || sat e f2
+ |
f1 ==> f2 ⇒ (
sat e f1 ==> sat e f2)%
bool
+ |
¬ f1 ⇒
~~ sat e f1
+ | (
'∃ 'X_k, f1) ⇒
[∃ x : F, sat (
set_nth 0%
R e k x)
f1]
+ | (
'∀ 'X_k, f1) ⇒
[∀ x : F, sat (
set_nth 0%
R e k x)
f1]
end%
T.
@@ -910,18 +1108,18 @@
Variable cT :
Field.type.
-
Let xT :=
let:
Field.Pack T _ _ :=
cT in T.
+
Let xT :=
let:
Field.Pack T _ :=
cT in T.
Let xclass :
Field.class_of xT :=
Field.class cT.
Definition type :=
Eval hnf in DecFieldType cT (
DecidableFieldMixin cT).
-
Definition finType := @
Finite.Pack type (
fin_ xclass)
xT.
-
Definition finZmodType := @
Zmodule.Pack type xclass xT.
-
Definition finRingType := @
Ring.Pack type xclass xT.
-
Definition finUnitRingType := @
UnitRing.Pack type xclass xT.
-
Definition finComRingType := @
ComRing.Pack type xclass xT.
-
Definition finComUnitRingType := @
ComUnitRing.Pack type xclass xT.
-
Definition finIdomainType := @
IntegralDomain.Pack type xclass xT.
+
Definition finType := @
Finite.Pack type (
fin_ xclass).
+
Definition finZmodType := @
Zmodule.Pack type xclass.
+
Definition finRingType := @
Ring.Pack type xclass.
+
Definition finUnitRingType := @
UnitRing.Pack type xclass.
+
Definition finComRingType := @
ComRing.Pack type xclass.
+
Definition finComUnitRingType := @
ComUnitRing.Pack type xclass.
+
Definition finIdomainType := @
IntegralDomain.Pack type xclass.
Definition baseFinGroupType :=
base_group type finZmodType finZmodType.
Definition finGroupType :=
fin_group baseFinGroupType cT.
@@ -941,6 +1139,8 @@
Canonical finIdomainType.
Canonical baseFinGroupType.
Canonical finGroupType.
+
+
End Exports.
@@ -958,32 +1158,34 @@
Record class_of M :=
Class {
base :
GRing.Lmodule.class_of R M;
mixin :
mixin_of M base }.
-
Definition base2 R (
c :
class_of R) :=
Zmodule.Class (
mixin c).
-
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
-
Variables (
phR :
phant R) (
cT :
type phR).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
+
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort}.
+
Variables (
phR :
phant R) (
cT :
type phR).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
Definition pack :=
gen_pack (
Pack phR)
Class (@
GRing.Lmodule.class R phR).
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition lmodType := @
GRing.Lmodule.Pack R phR cT xclass xT.
-
Definition join_finType := @
Finite.Pack lmodType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack lmodType xclass xT.
-
-
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition lmodType := @
GRing.Lmodule.Pack R phR cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group lmodType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition lmod_countType := @
Countable.Pack lmodType (
fin_ xclass).
+
Definition lmod_finType := @
Finite.Pack lmodType (
fin_ xclass).
+
Definition lmod_baseFinGroupType :=
base_group lmodType zmodType finType.
+
Definition lmod_finGroupType :=
fin_group lmod_baseFinGroupType zmodType.
+
Definition lmod_countZmodType := @
CountRing.Zmodule.Pack lmodType xclass.
+
Definition lmod_finZmodType := @
Zmodule.Pack lmodType xclass.
End ClassDef.
@@ -1001,21 +1203,27 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion lmodType : type >-> GRing.Lmodule.type.
Canonical lmodType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
-
Notation finLmodType R := (
FinRing.Lmodule.type (
Phant R)).
-
Notation "[ 'finLmodType' R 'of' T ]" := (
do_pack (@
pack _ (
Phant R))
T)
+
Canonical lmod_countType.
+
Canonical lmod_finType.
+
Canonical lmod_baseFinGroupType.
+
Canonical lmod_finGroupType.
+
Canonical lmod_countZmodType.
+
Canonical lmod_finZmodType.
+
Notation finLmodType R := (
FinRing.Lmodule.type (
Phant R)).
+
Notation "[ 'finLmodType' R 'of' T ]" := (
do_pack (@
pack _ (
Phant R))
T)
(
at level 0,
format "[ 'finLmodType' R 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -1038,40 +1246,45 @@
Definition base3 M (
c :
class_of M) := @
Lmodule.Class _ _ (
base c) (
mixin c).
-
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
-
Variables (
phR :
phant R) (
cT :
type phR).
+
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort}.
+
Variables (
phR :
phant R) (
cT :
type phR).
Definition pack :=
gen_pack (
Pack phR)
Class (@
GRing.Lalgebra.class R phR).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition finRingType := @
Ring.Pack cT xclass xT.
-
Definition lmodType := @
GRing.Lmodule.Pack R phR cT xclass xT.
-
Definition finLmodType := @
Lmodule.Pack R phR cT xclass xT.
-
Definition lalgType := @
GRing.Lalgebra.Pack R phR cT xclass xT.
-
-
-
Definition join_finType := @
Finite.Pack lalgType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack lalgType xclass xT.
-
Definition join_finLmodType := @
Lmodule.Pack R phR lalgType xclass xT.
-
Definition join_finRingType := @
Ring.Pack lalgType xclass xT.
-
Definition rjoin_finLmodType := @
Lmodule.Pack R phR ringType xclass xT.
-
Definition ljoin_finRingType := @
Ring.Pack lmodType xclass xT.
-
Definition fljoin_finRingType := @
Ring.Pack finLmodType xclass xT.
-
-
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition countRingType := @
CountRing.Ring.Pack cT xclass.
+
Definition finRingType := @
Ring.Pack cT xclass.
+
Definition lmodType := @
GRing.Lmodule.Pack R phR cT xclass.
+
Definition finLmodType := @
Lmodule.Pack R phR cT xclass.
+
Definition lalgType := @
GRing.Lalgebra.Pack R phR cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group lalgType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition lalg_countType := @
Countable.Pack lalgType (
fin_ xclass).
+
Definition lalg_finType := @
Finite.Pack lalgType (
fin_ xclass).
+
Definition lalg_baseFinGroupType :=
base_group lalgType zmodType finType.
+
Definition lalg_finGroupType :=
fin_group lalg_baseFinGroupType zmodType.
+
Definition lalg_countZmodType := @
CountRing.Zmodule.Pack lalgType xclass.
+
Definition lalg_finZmodType := @
Zmodule.Pack lalgType xclass.
+
Definition lalg_finLmodType := @
Lmodule.Pack R phR lalgType xclass.
+
Definition lalg_countRingType := @
CountRing.Ring.Pack lalgType xclass.
+
Definition lalg_finRingType := @
Ring.Pack lalgType xclass.
+
Definition lmod_countRingType := @
CountRing.Ring.Pack lmodType xclass.
+
Definition lmod_finRingType := @
Ring.Pack lmodType xclass.
+
Definition finLmod_ringType := @
GRing.Ring.Pack finLmodType xclass.
+
Definition finLmod_countRingType := @
CountRing.Ring.Pack finLmodType xclass.
+
Definition finLmod_finRingType := @
Ring.Pack finLmodType xclass.
End ClassDef.
@@ -1090,12 +1303,20 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
+
Coercion countRingType : type >-> CountRing.Ring.type.
+
Canonical countRingType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion lmodType : type >-> GRing.Lmodule.type.
@@ -1104,20 +1325,23 @@
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
-
Canonical join_finLmodType.
-
Canonical join_finRingType.
-
Canonical rjoin_finLmodType.
-
Canonical ljoin_finRingType.
-
Canonical fljoin_finRingType.
-
Notation finLalgType R := (
FinRing.Lalgebra.type (
Phant R)).
-
Notation "[ 'finLalgType' R 'of' T ]" := (
do_pack (@
pack _ (
Phant R))
T)
+
Canonical lalg_countType.
+
Canonical lalg_finType.
+
Canonical lalg_baseFinGroupType.
+
Canonical lalg_finGroupType.
+
Canonical lalg_countZmodType.
+
Canonical lalg_finZmodType.
+
Canonical lalg_finLmodType.
+
Canonical lalg_countRingType.
+
Canonical lalg_finRingType.
+
Canonical lmod_countRingType.
+
Canonical lmod_finRingType.
+
Canonical finLmod_ringType.
+
Canonical finLmod_countRingType.
+
Canonical finLmod_finRingType.
+
Notation finLalgType R := (
FinRing.Lalgebra.type (
Phant R)).
+
Notation "[ 'finLalgType' R 'of' T ]" := (
do_pack (@
pack _ (
Phant R))
T)
(
at level 0,
format "[ 'finLalgType' R 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -1139,40 +1363,43 @@
Definition base2 M (
c :
class_of M) :=
Lalgebra.Class (
mixin c).
-
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
-
Variables (
phR :
phant R) (
cT :
type phR).
+
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort}.
+
Variables (
phR :
phant R) (
cT :
type phR).
Definition pack :=
gen_pack (
Pack phR)
Class (@
GRing.Algebra.class R phR).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition finRingType := @
Ring.Pack cT xclass xT.
-
Definition lmodType := @
GRing.Lmodule.Pack R phR cT xclass xT.
-
Definition finLmodType := @
Lmodule.Pack R phR cT xclass xT.
-
Definition lalgType := @
GRing.Lalgebra.Pack R phR cT xclass xT.
-
Definition finLalgType := @
Lalgebra.Pack R phR cT xclass xT.
-
Definition algType := @
GRing.Algebra.Pack R phR cT xclass xT.
-
-
-
Definition join_finType := @
Finite.Pack algType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack algType xclass xT.
-
Definition join_finRingType := @
Ring.Pack algType xclass xT.
-
Definition join_finLmodType := @
Lmodule.Pack R phR algType xclass xT.
-
Definition join_finLalgType := @
Lalgebra.Pack R phR algType xclass xT.
-
-
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition countRingType := @
CountRing.Ring.Pack cT xclass.
+
Definition finRingType := @
Ring.Pack cT xclass.
+
Definition lmodType := @
GRing.Lmodule.Pack R phR cT xclass.
+
Definition finLmodType := @
Lmodule.Pack R phR cT xclass.
+
Definition lalgType := @
GRing.Lalgebra.Pack R phR cT xclass.
+
Definition finLalgType := @
Lalgebra.Pack R phR cT xclass.
+
Definition algType := @
GRing.Algebra.Pack R phR cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group algType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition alg_countType := @
Countable.Pack algType (
fin_ xclass).
+
Definition alg_finType := @
Finite.Pack algType (
fin_ xclass).
+
Definition alg_baseFinGroupType :=
base_group algType zmodType finType.
+
Definition alg_finGroupType :=
fin_group alg_baseFinGroupType zmodType.
+
Definition alg_countZmodType := @
CountRing.Zmodule.Pack algType xclass.
+
Definition alg_finZmodType := @
Zmodule.Pack algType xclass.
+
Definition alg_countRingType := @
CountRing.Ring.Pack algType xclass.
+
Definition alg_finRingType := @
Ring.Pack algType xclass.
+
Definition alg_finLmodType := @
Lmodule.Pack R phR algType xclass.
+
Definition alg_finLalgType := @
Lalgebra.Pack R phR algType xclass.
End ClassDef.
@@ -1190,12 +1417,20 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
+
Coercion countRingType : type >-> CountRing.Ring.type.
+
Canonical countRingType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion lmodType : type >-> GRing.Lmodule.type.
@@ -1208,18 +1443,19 @@
Canonical finLalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
-
Canonical join_finLmodType.
-
Canonical join_finRingType.
-
Canonical join_finLalgType.
-
Notation finAlgType R := (
type (
Phant R)).
-
Notation "[ 'finAlgType' R 'of' T ]" := (
do_pack (@
pack _ (
Phant R))
T)
+
Canonical alg_countType.
+
Canonical alg_finType.
+
Canonical alg_baseFinGroupType.
+
Canonical alg_finGroupType.
+
Canonical alg_countZmodType.
+
Canonical alg_finZmodType.
+
Canonical alg_countRingType.
+
Canonical alg_finRingType.
+
Canonical alg_finLmodType.
+
Canonical alg_finLalgType.
+
Notation finAlgType R := (
type (
Phant R)).
+
Notation "[ 'finAlgType' R 'of' T ]" := (
do_pack (@
pack _ (
Phant R))
T)
(
at level 0,
format "[ 'finAlgType' R 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -1236,7 +1472,7 @@
Variable R :
unitRingType.
-
Record class_of M :=
+
Record class_of M :=
Class {
base :
GRing.UnitAlgebra.class_of R M;
mixin :
mixin_of M base }.
Definition base2 M (
c :
class_of M) :=
Algebra.Class (
mixin c).
Definition base3 M (
c :
class_of M) := @
UnitRing.Class _ (
base c) (
mixin c).
@@ -1244,55 +1480,79 @@
-
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
-
Variables (
phR :
phant R) (
cT :
type phR).
+
Structure type (
phR :
phant R) :=
Pack {
sort;
_ :
class_of sort}.
+
Variables (
phR :
phant R) (
cT :
type phR).
Definition pack :=
gen_pack (
Pack phR)
Class (@
GRing.UnitAlgebra.class R phR).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
-
-
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
fin_ xclass)
xT.
-
Definition finType := @
Finite.Pack cT (
fin_ xclass)
xT.
-
Definition zmodType := @
GRing.Zmodule.Pack cT xclass xT.
-
Definition finZmodType := @
Zmodule.Pack cT xclass xT.
-
Definition ringType := @
GRing.Ring.Pack cT xclass xT.
-
Definition finRingType := @
Ring.Pack cT xclass xT.
-
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass xT.
-
Definition finUnitRingType := @
UnitRing.Pack cT xclass xT.
-
Definition lmodType := @
GRing.Lmodule.Pack R phR cT xclass xT.
-
Definition finLmodType := @
Lmodule.Pack R phR cT xclass xT.
-
Definition lalgType := @
GRing.Lalgebra.Pack R phR cT xclass xT.
-
Definition finLalgType := @
Lalgebra.Pack R phR cT xclass xT.
-
Definition algType := @
GRing.Algebra.Pack R phR cT xclass xT.
-
Definition finAlgType := @
Algebra.Pack R phR cT xclass xT.
-
Definition unitAlgType := @
GRing.UnitAlgebra.Pack R phR cT xclass xT.
-
-
-
Definition join_finType := @
Finite.Pack unitAlgType (
fin_ xclass)
xT.
-
Definition join_finZmodType := @
Zmodule.Pack unitAlgType xclass xT.
-
Definition join_finRingType := @
Ring.Pack unitAlgType xclass xT.
-
Definition join_finUnitRingType := @
UnitRing.Pack unitAlgType xclass xT.
-
Definition join_finLmodType := @
Lmodule.Pack R phR unitAlgType xclass xT.
-
Definition join_finLalgType := @
Lalgebra.Pack R phR unitAlgType xclass xT.
-
Definition join_finAlgType := @
Algebra.Pack R phR unitAlgType xclass xT.
-
Definition ljoin_finUnitRingType := @
UnitRing.Pack lmodType xclass xT.
-
Definition fljoin_finUnitRingType := @
UnitRing.Pack finLmodType xclass xT.
-
Definition njoin_finUnitRingType := @
UnitRing.Pack lalgType xclass xT.
-
Definition fnjoin_finUnitRingType := @
UnitRing.Pack finLalgType xclass xT.
-
Definition ajoin_finUnitRingType := @
UnitRing.Pack algType xclass xT.
-
Definition fajoin_finUnitRingType := @
UnitRing.Pack finAlgType xclass xT.
-
Definition ujoin_finLmodType := @
Lmodule.Pack R phR unitRingType xclass xT.
-
Definition ujoin_finLalgType := @
Lalgebra.Pack R phR unitRingType xclass xT.
-
Definition ujoin_finAlgType := @
Algebra.Pack R phR unitRingType xclass xT.
-
-
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
+
+
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
fin_ xclass).
+
Definition finType := @
Finite.Pack cT (
fin_ xclass).
+
Definition zmodType := @
GRing.Zmodule.Pack cT xclass.
+
Definition countZmodType := @
CountRing.Zmodule.Pack cT xclass.
+
Definition finZmodType := @
Zmodule.Pack cT xclass.
+
Definition ringType := @
GRing.Ring.Pack cT xclass.
+
Definition countRingType := @
CountRing.Ring.Pack cT xclass.
+
Definition finRingType := @
Ring.Pack cT xclass.
+
Definition unitRingType := @
GRing.UnitRing.Pack cT xclass.
+
Definition countUnitRingType := @
CountRing.UnitRing.Pack cT xclass.
+
Definition finUnitRingType := @
UnitRing.Pack cT xclass.
+
Definition lmodType := @
GRing.Lmodule.Pack R phR cT xclass.
+
Definition finLmodType := @
Lmodule.Pack R phR cT xclass.
+
Definition lalgType := @
GRing.Lalgebra.Pack R phR cT xclass.
+
Definition finLalgType := @
Lalgebra.Pack R phR cT xclass.
+
Definition algType := @
GRing.Algebra.Pack R phR cT xclass.
+
Definition finAlgType := @
Algebra.Pack R phR cT xclass.
+
Definition unitAlgType := @
GRing.UnitAlgebra.Pack R phR cT xclass.
Definition baseFinGroupType :=
base_group cT zmodType finType.
Definition finGroupType :=
fin_group baseFinGroupType zmodType.
-
Definition join_baseFinGroupType :=
base_group unitAlgType zmodType finType.
-
Definition join_finGroupType :=
fin_group join_baseFinGroupType zmodType.
+
+
+
Definition unitAlg_countType := @
Countable.Pack unitAlgType (
fin_ xclass).
+
Definition unitAlg_finType := @
Finite.Pack unitAlgType (
fin_ xclass).
+
Definition unitAlg_baseFinGroupType :=
base_group unitAlgType zmodType finType.
+
Definition unitAlg_finGroupType :=
fin_group unitAlg_baseFinGroupType zmodType.
+
Definition unitAlg_countZmodType := @
CountRing.Zmodule.Pack unitAlgType xclass.
+
Definition unitAlg_finZmodType := @
Zmodule.Pack unitAlgType xclass.
+
Definition unitAlg_countRingType := @
CountRing.Ring.Pack unitAlgType xclass.
+
Definition unitAlg_finRingType := @
Ring.Pack unitAlgType xclass.
+
Definition unitAlg_countUnitRingType :=
+ @
CountRing.UnitRing.Pack unitAlgType xclass.
+
Definition unitAlg_finUnitRingType := @
UnitRing.Pack unitAlgType xclass.
+
Definition unitAlg_finLmodType := @
Lmodule.Pack R phR unitAlgType xclass.
+
Definition unitAlg_finLalgType := @
Lalgebra.Pack R phR unitAlgType xclass.
+
Definition unitAlg_finAlgType := @
Algebra.Pack R phR unitAlgType xclass.
+
Definition unitRing_finLmodType := @
Lmodule.Pack R phR unitRingType xclass.
+
Definition unitRing_finLalgType := @
Lalgebra.Pack R phR unitRingType xclass.
+
Definition unitRing_finAlgType := @
Algebra.Pack R phR unitRingType xclass.
+
Definition countUnitRing_lmodType :=
+ @
GRing.Lmodule.Pack R phR countUnitRingType xclass.
+
Definition countUnitRing_finLmodType :=
+ @
Lmodule.Pack R phR countUnitRingType xclass.
+
Definition countUnitRing_lalgType :=
+ @
GRing.Lalgebra.Pack R phR countUnitRingType xclass.
+
Definition countUnitRing_finLalgType :=
+ @
Lalgebra.Pack R phR countUnitRingType xclass.
+
Definition countUnitRing_algType :=
+ @
GRing.Algebra.Pack R phR countUnitRingType xclass.
+
Definition countUnitRing_finAlgType :=
+ @
Algebra.Pack R phR countUnitRingType xclass.
+
Definition finUnitRing_lmodType :=
+ @
GRing.Lmodule.Pack R phR finUnitRingType xclass.
+
Definition finUnitRing_finLmodType :=
+ @
Lmodule.Pack R phR finUnitRingType xclass.
+
Definition finUnitRing_lalgType :=
+ @
GRing.Lalgebra.Pack R phR finUnitRingType xclass.
+
Definition finUnitRing_finLalgType :=
+ @
Lalgebra.Pack R phR finUnitRingType xclass.
+
Definition finUnitRing_algType :=
+ @
GRing.Algebra.Pack R phR finUnitRingType xclass.
+
Definition finUnitRing_finAlgType :=
+ @
Algebra.Pack R phR finUnitRingType xclass.
End ClassDef.
@@ -1311,16 +1571,26 @@
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
+
Coercion baseFinGroupType : type >-> FinGroup.base_type.
+
Canonical baseFinGroupType.
+
Coercion finGroupType : type >-> FinGroup.type.
+
Canonical finGroupType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
+
Coercion countZmodType : type >-> CountRing.Zmodule.type.
+
Canonical countZmodType.
Coercion finZmodType : type >-> Zmodule.type.
Canonical finZmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
+
Coercion countRingType : type >-> CountRing.Ring.type.
+
Canonical countRingType.
Coercion finRingType : type >-> Ring.type.
Canonical finRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
+
Coercion countUnitRingType : type >-> CountRing.UnitRing.type.
+
Canonical countUnitRingType.
Coercion finUnitRingType : type >-> UnitRing.type.
Canonical finUnitRingType.
Coercion lmodType : type >-> GRing.Lmodule.type.
@@ -1337,28 +1607,37 @@
Canonical finAlgType.
Coercion unitAlgType : type >-> GRing.UnitAlgebra.type.
Canonical unitAlgType.
-
Canonical join_finType.
-
Canonical join_finZmodType.
-
Canonical join_finLmodType.
-
Canonical join_finRingType.
-
Canonical join_finLalgType.
-
Canonical join_finAlgType.
-
Canonical ljoin_finUnitRingType.
-
Canonical fljoin_finUnitRingType.
-
Canonical njoin_finUnitRingType.
-
Canonical fnjoin_finUnitRingType.
-
Canonical ajoin_finUnitRingType.
-
Canonical fajoin_finUnitRingType.
-
Canonical ujoin_finLmodType.
-
Canonical ujoin_finLalgType.
-
Canonical ujoin_finAlgType.
-
Notation finUnitAlgType R := (
type (
Phant R)).
-
Notation "[ 'finUnitAlgType' R 'of' T ]" := (
do_pack (@
pack _ (
Phant R))
T)
+
Canonical unitAlg_countType.
+
Canonical unitAlg_finType.
+
Canonical unitAlg_baseFinGroupType.
+
Canonical unitAlg_finGroupType.
+
Canonical unitAlg_countZmodType.
+
Canonical unitAlg_finZmodType.
+
Canonical unitAlg_countRingType.
+
Canonical unitAlg_finRingType.
+
Canonical unitAlg_countUnitRingType.
+
Canonical unitAlg_finUnitRingType.
+
Canonical unitAlg_finLmodType.
+
Canonical unitAlg_finLalgType.
+
Canonical unitAlg_finAlgType.
+
Canonical unitRing_finLmodType.
+
Canonical unitRing_finLalgType.
+
Canonical unitRing_finAlgType.
+
Canonical countUnitRing_lmodType.
+
Canonical countUnitRing_finLmodType.
+
Canonical countUnitRing_lalgType.
+
Canonical countUnitRing_finLalgType.
+
Canonical countUnitRing_algType.
+
Canonical countUnitRing_finAlgType.
+
Canonical finUnitRing_lmodType.
+
Canonical finUnitRing_finLmodType.
+
Canonical finUnitRing_lalgType.
+
Canonical finUnitRing_finLalgType.
+
Canonical finUnitRing_algType.
+
Canonical finUnitRing_finAlgType.
+
Notation finUnitAlgType R := (
type (
Phant R)).
+
Notation "[ 'finUnitAlgType' R 'of' T ]" := (
do_pack (@
pack _ (
Phant R))
T)
(
at level 0,
format "[ 'finUnitAlgType' R 'of' T ]") :
form_scope.
-
Canonical baseFinGroupType.
-
Canonical finGroupType.
-
Canonical join_baseFinGroupType.
-
Canonical join_finGroupType.
End Exports.
@@ -1395,12 +1674,10 @@
Export Lmodule.Exports Lalgebra.Exports Algebra.Exports UnitAlgebra.Exports.
-
Notation "{ 'unit' R }" := (
unit_of (
Phant R))
+
Notation "{ 'unit' R }" := (
unit_of (
Phant R))
(
at level 0,
format "{ 'unit' R }") :
type_scope.
-
Notation "''U'" := (
unit_action _) (
at level 8) :
action_scope.
-
Notation "''U'" := (
unit_groupAction _) (
at level 8) :
groupAction_scope.
-
-
+
Notation "''U'" := (
unit_action _) (
at level 8) :
action_scope.
+
Notation "''U'" := (
unit_groupAction _) (
at level 8) :
groupAction_scope.