Library mathcomp.algebra.finalg
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype finset fingroup morphism perm action.
From mathcomp Require Import ssralg countalg.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype finset fingroup morphism perm action.
From mathcomp Require Import ssralg countalg.
This file clones the entire ssralg hierachy for finite types; this allows
type inference to function properly on expressions that mix combinatorial
and algebraic operators (e.g., [set x + y | x in A, y in A]).
finZmodType, finRingType, finComRingType, finUnitRingType,
finComUnitRingType, finIdomType, finFieldType finLmodType,
finLalgType finAlgType finUnitAlgType
== the finite counterparts of zmodType, etc.
Note that a finFieldType is canonically decidable. All these structures
can be derived using [xxxType of T] forms, e.g., if R has both canonical
finType and ringType structures, then
Canonical R_finRingType := Eval hnf in [finRingType of R].
declares the derived finRingType structure for R. As the implementation
of the derivation is somewhat involved, the Eval hnf normalization is
strongly recommended.
This file also provides direct tie-ins with finite group theory:
[baseFinGroupType of R for +%R] == the (canonical) additive group
[finGroupType of R for +%R] structures for R
{unit R} == the type of units of R, which has a
canonical group structure.
FinRing.unit R Ux == the element of {unit R} corresponding
to x, where Ux : x \in GRing.unit.
'U%act == the action by right multiplication of
{unit R} on R, via FinRing.unit_act.
(This is also a group action.)
Implicits
Variables (type base_type : Type) (class_of base_of : Type → Type).
Variable to_choice : ∀ T, base_of T → Choice.class_of T.
Variable base_sort : base_type → Type.
Variable to_choice : ∀ T, base_of T → Choice.class_of T.
Variable base_sort : base_type → Type.
Explicits
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).
End Generic.
Import GRing.Theory.
Definition groupMixin V := FinGroup.Mixin (@addrA V) (@add0r V) (@addNr V).
Module Zmodule.
Section ClassDef.
Record class_of M :=
Class { base : GRing.Zmodule.class_of M; mixin : mixin_of M base }.
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.
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 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.
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.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finGroupType' 'of' R 'for' +%R ]") : form_scope.
End Exports.
End Zmodule.
Import Zmodule.Exports.
Section AdditiveGroup.
Variable U : finZmodType.
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 zmod_mulgC x y : commute x y.
Lemma zmod_abelian (A : {set U}) : abelian A.
End AdditiveGroup.
Module Ring.
Section ClassDef.
Record class_of R :=
Class { base : GRing.Ring.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Import Exports.
Coercion base : class_of >-> GRing.Ring.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finRingType' 'of' T ]") : form_scope.
End Exports.
Section Unit.
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)).
Lemma mulVr : {in unit, left_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 invr_out : {in [predC unit], inv =1 id}.
Definition UnitMixin := GRing.UnitRing.Mixin mulVr mulrV intro_unit invr_out.
End Unit.
End Ring.
Import Ring.Exports.
Module ComRing.
Section ClassDef.
Record class_of R :=
Class { base : GRing.ComRing.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.ComRing.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finComRingType' 'of' T ]") : form_scope.
End Exports.
End ComRing.
Import ComRing.Exports.
Module UnitRing.
Section ClassDef.
Record class_of R :=
Class { base : GRing.UnitRing.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.UnitRing.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finUnitRingType' 'of' T ]") : form_scope.
End Exports.
End UnitRing.
Import UnitRing.Exports.
Section UnitsGroup.
Variable R : finUnitRingType.
Inductive unit_of (phR : phant R) := Unit (x : R) of x \is a GRing.unit.
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_eqType := Eval hnf in EqType uT unit_eqMixin.
Definition unit_choiceMixin := [choiceMixin of uT by <:].
Canonical unit_choiceType := Eval hnf in ChoiceType uT unit_choiceMixin.
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_finType := Eval hnf in FinType uT unit_finMixin.
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.
Definition unit_inv u := Unit phR (unit_inv_proof u).
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.
Definition unit_GroupMixin := FinGroup.Mixin unit_muluA unit_mul1u unit_mulVu.
Canonical unit_baseFinGroupType :=
Eval hnf in BaseFinGroupType uT unit_GroupMixin.
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.
Definition unit_act x u := x × val u.
Lemma unit_actE x u : unit_act x u = x × val u.
Canonical unit_action :=
@TotalAction _ _ unit_act (@GRing.mulr1 _) (fun _ _ _ ⇒ GRing.mulrA _ _ _).
Lemma unit_is_groupAction : @is_groupAction _ R setT setT unit_action.
Canonical unit_groupAction := GroupAction unit_is_groupAction.
End UnitsGroup.
Module Import UnitsGroupExports.
Canonical unit_subType.
Canonical unit_eqType.
Canonical unit_choiceType.
Canonical unit_countType.
Canonical unit_subCountType.
Canonical unit_finType.
Canonical unit_subFinType.
Canonical unit_baseFinGroupType.
Canonical unit_finGroupType.
Canonical unit_action.
Canonical unit_groupAction.
End UnitsGroupExports.
Notation unit R Ux := (Unit (Phant R) Ux).
Module ComUnitRing.
Section ClassDef.
Record class_of R :=
Class { base : GRing.ComUnitRing.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.ComUnitRing.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finComUnitRingType' 'of' T ]") : form_scope.
End Exports.
End ComUnitRing.
Import ComUnitRing.Exports.
Module IntegralDomain.
Section ClassDef.
Record class_of R :=
Class { base : GRing.IntegralDomain.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.IntegralDomain.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finIdomainType' 'of' T ]") : form_scope.
End Exports.
End IntegralDomain.
Import IntegralDomain.Exports.
Module Field.
Section ClassDef.
Record class_of R :=
Class { base : GRing.Field.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.Field.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finFieldType' 'of' T ]") : form_scope.
End Exports.
End Field.
Import Field.Exports.
Section DecideField.
Variable F : Field.type.
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]
end%T.
Lemma decidable : GRing.DecidableField.axiom sat.
Definition DecidableFieldMixin := DecFieldMixin decidable.
End DecideField.
Module DecField.
Section Joins.
Variable cT : Field.type.
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).
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.
End Joins.
Module Exports.
Coercion type : Field.type >-> GRing.DecidableField.type.
Canonical type.
Canonical finType.
Canonical finZmodType.
Canonical finRingType.
Canonical finUnitRingType.
Canonical finComRingType.
Canonical finComUnitRingType.
Canonical finIdomainType.
Canonical baseFinGroupType.
Canonical finGroupType.
End Exports.
End DecField.
Module Lmodule.
Section ClassDef.
Variable R : ringType.
Record class_of M :=
Class { base : GRing.Lmodule.class_of R M; mixin : mixin_of M base }.
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.
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 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.
Module Import Exports.
Coercion base : class_of >-> GRing.Lmodule.class_of.
Coercion base2 : class_of >-> Zmodule.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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 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.
End Exports.
End Lmodule.
Import Lmodule.Exports.
Module Lalgebra.
Section ClassDef.
Variable R : ringType.
Record class_of M :=
Class { base : GRing.Lalgebra.class_of R M; mixin : mixin_of M base }.
Definition base2 M (c : class_of M) := Ring.Class (mixin c).
Definition base3 M (c : class_of M) := @Lmodule.Class _ _ (base c) (mixin c).
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.Lalgebra.class_of.
Coercion base2 : class_of >-> Ring.class_of.
Coercion base3 : class_of >-> Lmodule.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
Canonical lmodType.
Coercion finLmodType : type >-> Lmodule.type.
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
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.
End Exports.
End Lalgebra.
Import Lalgebra.Exports.
Module Algebra.
Section ClassDef.
Variable R : ringType.
Record class_of M :=
Class { base : GRing.Algebra.class_of R M; mixin : mixin_of M base }.
Definition base2 M (c : class_of M) := Lalgebra.Class (mixin c).
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.Algebra.class_of.
Coercion base2 : class_of >-> Lalgebra.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
Canonical lmodType.
Coercion finLmodType : type >-> Lmodule.type.
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Coercion finLalgType : type >-> Lalgebra.type.
Canonical finLalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
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.
End Exports.
End Algebra.
Import Algebra.Exports.
Module UnitAlgebra.
Section ClassDef.
Variable R : unitRingType.
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).
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.UnitAlgebra.class_of.
Coercion base2 : class_of >-> Algebra.class_of.
Coercion base3 : class_of >-> UnitRing.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
Canonical lmodType.
Coercion finLmodType : type >-> Lmodule.type.
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Coercion finLalgType : type >-> Lalgebra.type.
Canonical finLalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
Coercion finAlgType : type >-> Algebra.type.
Canonical finAlgType.
Coercion unitAlgType : type >-> GRing.UnitAlgebra.type.
Canonical unitAlgType.
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.
End Exports.
End UnitAlgebra.
Import UnitAlgebra.Exports.
Module Theory.
Definition zmod1gE := zmod1gE.
Definition zmodVgE := zmodVgE.
Definition zmodMgE := zmodMgE.
Definition zmodXgE := zmodXgE.
Definition zmod_mulgC := zmod_mulgC.
Definition zmod_abelian := zmod_abelian.
Definition val_unit1 := val_unit1.
Definition val_unitM := val_unitM.
Definition val_unitX := val_unitX.
Definition val_unitV := val_unitV.
Definition unit_actE := unit_actE.
End Theory.
End FinRing.
Import FinRing.
Export Zmodule.Exports Ring.Exports ComRing.Exports.
Export UnitRing.Exports UnitsGroupExports ComUnitRing.Exports.
Export IntegralDomain.Exports Field.Exports DecField.Exports.
Export Lmodule.Exports Lalgebra.Exports Algebra.Exports UnitAlgebra.Exports.
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.
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).
End Generic.
Import GRing.Theory.
Definition groupMixin V := FinGroup.Mixin (@addrA V) (@add0r V) (@addNr V).
Module Zmodule.
Section ClassDef.
Record class_of M :=
Class { base : GRing.Zmodule.class_of M; mixin : mixin_of M base }.
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.
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 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.
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.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finGroupType' 'of' R 'for' +%R ]") : form_scope.
End Exports.
End Zmodule.
Import Zmodule.Exports.
Section AdditiveGroup.
Variable U : finZmodType.
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 zmod_mulgC x y : commute x y.
Lemma zmod_abelian (A : {set U}) : abelian A.
End AdditiveGroup.
Module Ring.
Section ClassDef.
Record class_of R :=
Class { base : GRing.Ring.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Import Exports.
Coercion base : class_of >-> GRing.Ring.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finRingType' 'of' T ]") : form_scope.
End Exports.
Section Unit.
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)).
Lemma mulVr : {in unit, left_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 invr_out : {in [predC unit], inv =1 id}.
Definition UnitMixin := GRing.UnitRing.Mixin mulVr mulrV intro_unit invr_out.
End Unit.
End Ring.
Import Ring.Exports.
Module ComRing.
Section ClassDef.
Record class_of R :=
Class { base : GRing.ComRing.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.ComRing.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finComRingType' 'of' T ]") : form_scope.
End Exports.
End ComRing.
Import ComRing.Exports.
Module UnitRing.
Section ClassDef.
Record class_of R :=
Class { base : GRing.UnitRing.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.UnitRing.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finUnitRingType' 'of' T ]") : form_scope.
End Exports.
End UnitRing.
Import UnitRing.Exports.
Section UnitsGroup.
Variable R : finUnitRingType.
Inductive unit_of (phR : phant R) := Unit (x : R) of x \is a GRing.unit.
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_eqType := Eval hnf in EqType uT unit_eqMixin.
Definition unit_choiceMixin := [choiceMixin of uT by <:].
Canonical unit_choiceType := Eval hnf in ChoiceType uT unit_choiceMixin.
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_finType := Eval hnf in FinType uT unit_finMixin.
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.
Definition unit_inv u := Unit phR (unit_inv_proof u).
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.
Definition unit_GroupMixin := FinGroup.Mixin unit_muluA unit_mul1u unit_mulVu.
Canonical unit_baseFinGroupType :=
Eval hnf in BaseFinGroupType uT unit_GroupMixin.
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.
Definition unit_act x u := x × val u.
Lemma unit_actE x u : unit_act x u = x × val u.
Canonical unit_action :=
@TotalAction _ _ unit_act (@GRing.mulr1 _) (fun _ _ _ ⇒ GRing.mulrA _ _ _).
Lemma unit_is_groupAction : @is_groupAction _ R setT setT unit_action.
Canonical unit_groupAction := GroupAction unit_is_groupAction.
End UnitsGroup.
Module Import UnitsGroupExports.
Canonical unit_subType.
Canonical unit_eqType.
Canonical unit_choiceType.
Canonical unit_countType.
Canonical unit_subCountType.
Canonical unit_finType.
Canonical unit_subFinType.
Canonical unit_baseFinGroupType.
Canonical unit_finGroupType.
Canonical unit_action.
Canonical unit_groupAction.
End UnitsGroupExports.
Notation unit R Ux := (Unit (Phant R) Ux).
Module ComUnitRing.
Section ClassDef.
Record class_of R :=
Class { base : GRing.ComUnitRing.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.ComUnitRing.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finComUnitRingType' 'of' T ]") : form_scope.
End Exports.
End ComUnitRing.
Import ComUnitRing.Exports.
Module IntegralDomain.
Section ClassDef.
Record class_of R :=
Class { base : GRing.IntegralDomain.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.IntegralDomain.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finIdomainType' 'of' T ]") : form_scope.
End Exports.
End IntegralDomain.
Import IntegralDomain.Exports.
Module Field.
Section ClassDef.
Record class_of R :=
Class { base : GRing.Field.class_of R; mixin : mixin_of R base }.
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.Field.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.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
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)
(at level 0, format "[ 'finFieldType' 'of' T ]") : form_scope.
End Exports.
End Field.
Import Field.Exports.
Section DecideField.
Variable F : Field.type.
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]
end%T.
Lemma decidable : GRing.DecidableField.axiom sat.
Definition DecidableFieldMixin := DecFieldMixin decidable.
End DecideField.
Module DecField.
Section Joins.
Variable cT : Field.type.
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).
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.
End Joins.
Module Exports.
Coercion type : Field.type >-> GRing.DecidableField.type.
Canonical type.
Canonical finType.
Canonical finZmodType.
Canonical finRingType.
Canonical finUnitRingType.
Canonical finComRingType.
Canonical finComUnitRingType.
Canonical finIdomainType.
Canonical baseFinGroupType.
Canonical finGroupType.
End Exports.
End DecField.
Module Lmodule.
Section ClassDef.
Variable R : ringType.
Record class_of M :=
Class { base : GRing.Lmodule.class_of R M; mixin : mixin_of M base }.
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.
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 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.
Module Import Exports.
Coercion base : class_of >-> GRing.Lmodule.class_of.
Coercion base2 : class_of >-> Zmodule.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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 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.
End Exports.
End Lmodule.
Import Lmodule.Exports.
Module Lalgebra.
Section ClassDef.
Variable R : ringType.
Record class_of M :=
Class { base : GRing.Lalgebra.class_of R M; mixin : mixin_of M base }.
Definition base2 M (c : class_of M) := Ring.Class (mixin c).
Definition base3 M (c : class_of M) := @Lmodule.Class _ _ (base c) (mixin c).
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.Lalgebra.class_of.
Coercion base2 : class_of >-> Ring.class_of.
Coercion base3 : class_of >-> Lmodule.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
Canonical lmodType.
Coercion finLmodType : type >-> Lmodule.type.
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
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.
End Exports.
End Lalgebra.
Import Lalgebra.Exports.
Module Algebra.
Section ClassDef.
Variable R : ringType.
Record class_of M :=
Class { base : GRing.Algebra.class_of R M; mixin : mixin_of M base }.
Definition base2 M (c : class_of M) := Lalgebra.Class (mixin c).
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.Algebra.class_of.
Coercion base2 : class_of >-> Lalgebra.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
Canonical lmodType.
Coercion finLmodType : type >-> Lmodule.type.
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Coercion finLalgType : type >-> Lalgebra.type.
Canonical finLalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
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.
End Exports.
End Algebra.
Import Algebra.Exports.
Module UnitAlgebra.
Section ClassDef.
Variable R : unitRingType.
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).
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.
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 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.
Module Exports.
Coercion base : class_of >-> GRing.UnitAlgebra.class_of.
Coercion base2 : class_of >-> Algebra.class_of.
Coercion base3 : class_of >-> UnitRing.class_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
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.
Canonical lmodType.
Coercion finLmodType : type >-> Lmodule.type.
Canonical finLmodType.
Coercion lalgType : type >-> GRing.Lalgebra.type.
Canonical lalgType.
Coercion finLalgType : type >-> Lalgebra.type.
Canonical finLalgType.
Coercion algType : type >-> GRing.Algebra.type.
Canonical algType.
Coercion finAlgType : type >-> Algebra.type.
Canonical finAlgType.
Coercion unitAlgType : type >-> GRing.UnitAlgebra.type.
Canonical unitAlgType.
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.
End Exports.
End UnitAlgebra.
Import UnitAlgebra.Exports.
Module Theory.
Definition zmod1gE := zmod1gE.
Definition zmodVgE := zmodVgE.
Definition zmodMgE := zmodMgE.
Definition zmodXgE := zmodXgE.
Definition zmod_mulgC := zmod_mulgC.
Definition zmod_abelian := zmod_abelian.
Definition val_unit1 := val_unit1.
Definition val_unitM := val_unitM.
Definition val_unitX := val_unitX.
Definition val_unitV := val_unitV.
Definition unit_actE := unit_actE.
End Theory.
End FinRing.
Import FinRing.
Export Zmodule.Exports Ring.Exports ComRing.Exports.
Export UnitRing.Exports UnitsGroupExports ComUnitRing.Exports.
Export IntegralDomain.Exports Field.Exports DecField.Exports.
Export Lmodule.Exports Lalgebra.Exports Algebra.Exports UnitAlgebra.Exports.
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.