diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/Make | 1 | ||||
| -rw-r--r-- | mathcomp/algebra/all_algebra.v | 1 | ||||
| -rw-r--r-- | mathcomp/algebra/countalg.v | 797 | ||||
| -rw-r--r-- | mathcomp/algebra/finalg.v | 59 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 32 | ||||
| -rw-r--r-- | mathcomp/algebra/rat.v | 10 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 9 | ||||
| -rw-r--r-- | mathcomp/algebra/zmodp.v | 11 |
9 files changed, 918 insertions, 11 deletions
diff --git a/mathcomp/algebra/Make b/mathcomp/algebra/Make index 7d12cb4..b3001f9 100644 --- a/mathcomp/algebra/Make +++ b/mathcomp/algebra/Make @@ -1,4 +1,5 @@ all_algebra.v +countalg.v finalg.v fraction.v intdiv.v diff --git a/mathcomp/algebra/all_algebra.v b/mathcomp/algebra/all_algebra.v index 8a31d60..a937b0c 100644 --- a/mathcomp/algebra/all_algebra.v +++ b/mathcomp/algebra/all_algebra.v @@ -1,6 +1,7 @@ Require Export ssralg. Require Export ssrnum. Require Export finalg. +Require Export countalg. Require Export poly. Require Export polydiv. Require Export polyXY. diff --git a/mathcomp/algebra/countalg.v b/mathcomp/algebra/countalg.v new file mode 100644 index 0000000..21000e4 --- /dev/null +++ b/mathcomp/algebra/countalg.v @@ -0,0 +1,797 @@ +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) +Require Import mathcomp.ssreflect.ssreflect. +From mathcomp +Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. +From mathcomp +Require Import bigop ssralg generic_quotient ring_quotient. + +(*****************************************************************************) +(* This file clones part of ssralg hierachy for countable types; it does not *) +(* cover the left module / algebra interfaces, providing only *) +(* countZmodType == countable zmodType interface. *) +(* countRingType == countable ringType interface. *) +(* countComRingType == countable comRingType interface. *) +(* countUnitRingType == countable unitRingType interface. *) +(* countComUnitRingType == countable comUnitRingType interface. *) +(* countIdomainType == countable idomainType interface. *) +(* countFieldType == countable fieldType interface. *) +(* countDecFieldType == countable decFieldType interface. *) +(* countClosedFieldType == countable closedFieldType interface. *) +(* The interface cloning syntax is extended to these structures *) +(* [countZmodType of M] == countZmodType structure for an M that has both *) +(* zmodType and countType structures. *) +(* ... etc *) +(* This file provides constructions for both simple extension and algebraic *) +(* closure of countable fields. *) +(*****************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. +Import GRing.Theory CodeSeq. + +Module CountRing. + +Local Notation mixin_of T := (Countable.mixin_of T). + +Section Generic. + +(* Implicits *) +Variables (type base_type : Type) (class_of base_of : Type -> Type). +Variable base_sort : base_type -> Type. + +(* Explicits *) +Variable Pack : forall T, class_of T -> Type -> type. +Variable Class : forall T, base_of T -> mixin_of T -> class_of T. +Variable base_class : forall bT, base_of (base_sort bT). + +Definition gen_pack T := + fun bT b & phant_id (base_class bT) b => + fun fT c m & phant_id (Countable.class fT) (Countable.Class c m) => + Pack (@Class T b m) T. + +End Generic. + +Arguments gen_pack [type base_type class_of base_of base_sort]. +Local Notation cnt_ c := (@Countable.Class _ c c). +Local Notation do_pack pack T := (pack T _ _ id _ _ _ id). +Import GRing.Theory. + +Module Zmodule. + +Section ClassDef. + +Record class_of M := + Class { base : GRing.Zmodule.class_of M; mixin : mixin_of M }. +Local Coercion base : class_of >-> GRing.Zmodule.class_of. +Local Coercion mixin : class_of >-> mixin_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Definition pack := gen_pack Pack Class GRing.Zmodule.class. +Variable cT : type. +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (cnt_ xclass) xT. +Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. + +Definition join_countType := @Countable.Pack zmodType (cnt_ xclass) xT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> GRing.Zmodule.class_of. +Coercion mixin : class_of >-> mixin_of. +Coercion sort : type >-> Sortclass. +Bind Scope ring_scope with sort. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical zmodType. +Canonical join_countType. +Notation countZmodType := type. +Notation "[ 'countZmodType' 'of' T ]" := (do_pack pack T) + (at level 0, format "[ 'countZmodType' 'of' T ]") : form_scope. +End Exports. + +End Zmodule. +Import Zmodule.Exports. + +Module Ring. + +Section ClassDef. + +Record class_of R := Class { base : GRing.Ring.class_of R; mixin : mixin_of R }. +Definition base2 R (c : class_of R) := Zmodule.Class (base c) (mixin c). +Local Coercion base : class_of >-> GRing.Ring.class_of. +Local Coercion base2 : class_of >-> Zmodule.class_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Definition pack := gen_pack Pack Class GRing.Ring.class. +Variable cT : type. +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (cnt_ xclass) xT. +Definition zmodType := @GRing.Zmodule.Pack cT xclass cT. +Definition countZmodType := @Zmodule.Pack cT xclass xT. +Definition ringType := @GRing.Ring.Pack cT xclass xT. +Definition join_countType := @Countable.Pack ringType (cnt_ xclass) xT. +Definition join_countZmodType := @Zmodule.Pack ringType xclass xT. + +End ClassDef. + +Module Import Exports. +Coercion base : class_of >-> GRing.Ring.class_of. +Coercion base2 : class_of >-> Zmodule.class_of. +Coercion sort : type >-> Sortclass. +Bind Scope ring_scope with sort. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical zmodType. +Coercion countZmodType : type >-> Zmodule.type. +Canonical countZmodType. +Coercion ringType : type >-> GRing.Ring.type. +Canonical ringType. +Canonical join_countType. +Canonical join_countZmodType. +Notation countRingType := type. +Notation "[ 'countRingType' 'of' T ]" := (do_pack pack T) + (at level 0, format "[ 'countRingType' 'of' T ]") : form_scope. +End Exports. + +End Ring. +Import Ring.Exports. + +Module ComRing. + +Section ClassDef. + +Record class_of R := + Class { base : GRing.ComRing.class_of R; mixin : mixin_of R }. +Definition base2 R (c : class_of R) := Ring.Class (base c) (mixin c). +Local Coercion base : class_of >-> GRing.ComRing.class_of. +Local Coercion base2 : class_of >-> Ring.class_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Definition pack := gen_pack Pack Class GRing.ComRing.class. +Variable cT : type. +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (cnt_ xclass) xT. +Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. +Definition countZmodType := @Zmodule.Pack cT xclass xT. +Definition ringType := @GRing.Ring.Pack cT xclass xT. +Definition countRingType := @Ring.Pack cT xclass xT. +Definition comRingType := @GRing.ComRing.Pack cT xclass xT. +Definition join_countType := @Countable.Pack comRingType (cnt_ xclass) xT. +Definition join_countZmodType := @Zmodule.Pack comRingType xclass xT. +Definition join_countRingType := @Ring.Pack comRingType xclass xT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> GRing.ComRing.class_of. +Coercion base2 : class_of >-> Ring.class_of. +Coercion sort : type >-> Sortclass. +Bind Scope ring_scope with sort. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical zmodType. +Coercion countZmodType : type >-> Zmodule.type. +Canonical countZmodType. +Coercion ringType : type >-> GRing.Ring.type. +Canonical ringType. +Coercion countRingType : type >-> Ring.type. +Canonical countRingType. +Coercion comRingType : type >-> GRing.ComRing.type. +Canonical comRingType. +Canonical join_countType. +Canonical join_countZmodType. +Canonical join_countRingType. +Notation countComRingType := CountRing.ComRing.type. +Notation "[ 'countComRingType' 'of' T ]" := (do_pack pack T) + (at level 0, format "[ 'countComRingType' '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 }. +Definition base2 R (c : class_of R) := Ring.Class (base c) (mixin c). +Local Coercion base : class_of >-> GRing.UnitRing.class_of. +Local Coercion base2 : class_of >-> Ring.class_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Definition pack := gen_pack Pack Class GRing.UnitRing.class. +Variable cT : type. +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (cnt_ xclass) xT. +Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. +Definition countZmodType := @Zmodule.Pack cT xclass xT. +Definition ringType := @GRing.Ring.Pack cT xclass xT. +Definition countRingType := @Ring.Pack cT xclass xT. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. + +Definition join_countType := @Countable.Pack unitRingType (cnt_ xclass) xT. +Definition join_countZmodType := @Zmodule.Pack unitRingType xclass xT. +Definition join_countRingType := @Ring.Pack unitRingType xclass xT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> GRing.UnitRing.class_of. +Coercion base2 : class_of >-> Ring.class_of. +Coercion sort : type >-> Sortclass. +Bind Scope ring_scope with sort. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical zmodType. +Coercion countZmodType : type >-> Zmodule.type. +Canonical countZmodType. +Coercion ringType : type >-> GRing.Ring.type. +Canonical ringType. +Coercion countRingType : type >-> Ring.type. +Canonical countRingType. +Coercion unitRingType : type >-> GRing.UnitRing.type. +Canonical unitRingType. +Canonical join_countType. +Canonical join_countZmodType. +Canonical join_countRingType. +Notation countUnitRingType := CountRing.UnitRing.type. +Notation "[ 'countUnitRingType' 'of' T ]" := (do_pack pack T) + (at level 0, format "[ 'countUnitRingType' 'of' T ]") : form_scope. +End Exports. + +End UnitRing. +Import UnitRing.Exports. + +Module ComUnitRing. + +Section ClassDef. + +Record class_of R := + Class { base : GRing.ComUnitRing.class_of R; mixin : mixin_of R }. +Definition base2 R (c : class_of R) := ComRing.Class (base c) (mixin c). +Definition base3 R (c : class_of R) := @UnitRing.Class R (base c) (mixin c). +Local Coercion base : class_of >-> GRing.ComUnitRing.class_of. +Local Coercion base2 : class_of >-> ComRing.class_of. +Local Coercion base3 : class_of >-> UnitRing.class_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Definition pack := gen_pack Pack Class GRing.ComUnitRing.class. +Variable cT : type. +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (cnt_ xclass) xT. +Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. +Definition countZmodType := @Zmodule.Pack cT xclass xT. +Definition ringType := @GRing.Ring.Pack cT xclass xT. +Definition countRingType := @Ring.Pack cT xclass xT. +Definition comRingType := @GRing.ComRing.Pack cT xclass xT. +Definition countComRingType := @ComRing.Pack cT xclass xT. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. +Definition countUnitRingType := @UnitRing.Pack cT xclass xT. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. + +Definition join_countType := @Countable.Pack comUnitRingType (cnt_ xclass) xT. +Definition join_countZmodType := @Zmodule.Pack comUnitRingType xclass xT. +Definition join_countRingType := @Ring.Pack comUnitRingType xclass xT. +Definition join_countComRingType := @ComRing.Pack comUnitRingType xclass xT. +Definition join_countUnitRingType := @UnitRing.Pack comUnitRingType xclass xT. +Definition ujoin_countComRingType := @ComRing.Pack unitRingType xclass xT. +Definition cjoin_countUnitRingType := @UnitRing.Pack comRingType xclass xT. +Definition ccjoin_countUnitRingType := + @UnitRing.Pack countComRingType xclass xT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> GRing.ComUnitRing.class_of. +Coercion base2 : class_of >-> ComRing.class_of. +Coercion base3 : class_of >-> UnitRing.class_of. +Coercion sort : type >-> Sortclass. +Bind Scope ring_scope with sort. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical zmodType. +Coercion countZmodType : type >-> Zmodule.type. +Canonical countZmodType. +Coercion ringType : type >-> GRing.Ring.type. +Canonical ringType. +Coercion countRingType : type >-> Ring.type. +Canonical countRingType. +Coercion comRingType : type >-> GRing.ComRing.type. +Canonical comRingType. +Coercion countComRingType : type >-> ComRing.type. +Canonical countComRingType. +Coercion unitRingType : type >-> GRing.UnitRing.type. +Canonical unitRingType. +Coercion countUnitRingType : type >-> UnitRing.type. +Canonical countUnitRingType. +Coercion comUnitRingType : type >-> GRing.ComUnitRing.type. +Canonical comUnitRingType. +Canonical join_countType. +Canonical join_countZmodType. +Canonical join_countRingType. +Canonical join_countComRingType. +Canonical join_countUnitRingType. +Canonical ujoin_countComRingType. +Canonical cjoin_countUnitRingType. +Canonical ccjoin_countUnitRingType. +Notation countComUnitRingType := CountRing.ComUnitRing.type. +Notation "[ 'countComUnitRingType' 'of' T ]" := (do_pack pack T) + (at level 0, format "[ 'countComUnitRingType' '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 }. +Definition base2 R (c : class_of R) := ComUnitRing.Class (base c) (mixin c). +Local Coercion base : class_of >-> GRing.IntegralDomain.class_of. +Local Coercion base2 : class_of >-> ComUnitRing.class_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Definition pack := gen_pack Pack Class GRing.IntegralDomain.class. +Variable cT : type. +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (cnt_ xclass) xT. +Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. +Definition countZmodType := @Zmodule.Pack cT xclass xT. +Definition ringType := @GRing.Ring.Pack cT xclass xT. +Definition countRingType := @Ring.Pack cT xclass xT. +Definition comRingType := @GRing.ComRing.Pack cT xclass xT. +Definition countComRingType := @ComRing.Pack cT xclass xT. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. +Definition countUnitRingType := @UnitRing.Pack cT xclass xT. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. +Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. + +Definition join_countType := @Countable.Pack idomainType (cnt_ xclass) xT. +Definition join_countZmodType := @Zmodule.Pack idomainType xclass xT. +Definition join_countRingType := @Ring.Pack idomainType xclass xT. +Definition join_countUnitRingType := @UnitRing.Pack idomainType xclass xT. +Definition join_countComRingType := @ComRing.Pack idomainType xclass xT. +Definition join_countComUnitRingType := @ComUnitRing.Pack idomainType xclass xT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> GRing.IntegralDomain.class_of. +Coercion base2 : class_of >-> ComUnitRing.class_of. +Coercion sort : type >-> Sortclass. +Bind Scope ring_scope with sort. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical zmodType. +Coercion countZmodType : type >-> Zmodule.type. +Canonical countZmodType. +Coercion ringType : type >-> GRing.Ring.type. +Canonical ringType. +Coercion countRingType : type >-> Ring.type. +Canonical countRingType. +Coercion comRingType : type >-> GRing.ComRing.type. +Canonical comRingType. +Coercion countComRingType : type >-> ComRing.type. +Canonical countComRingType. +Coercion unitRingType : type >-> GRing.UnitRing.type. +Canonical unitRingType. +Coercion countUnitRingType : type >-> UnitRing.type. +Canonical countUnitRingType. +Coercion comUnitRingType : type >-> GRing.ComUnitRing.type. +Canonical comUnitRingType. +Coercion countComUnitRingType : type >-> ComUnitRing.type. +Canonical countComUnitRingType. +Coercion idomainType : type >-> GRing.IntegralDomain.type. +Canonical idomainType. +Canonical join_countType. +Canonical join_countZmodType. +Canonical join_countRingType. +Canonical join_countComRingType. +Canonical join_countUnitRingType. +Canonical join_countComUnitRingType. +Notation countIdomainType := CountRing.IntegralDomain.type. +Notation "[ 'countIdomainType' 'of' T ]" := (do_pack pack T) + (at level 0, format "[ 'countIdomainType' '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 }. +Definition base2 R (c : class_of R) := IntegralDomain.Class (base c) (mixin c). +Local Coercion base : class_of >-> GRing.Field.class_of. +Local Coercion base2 : class_of >-> IntegralDomain.class_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Definition pack := gen_pack Pack Class GRing.Field.class. +Variable cT : type. +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (cnt_ xclass) xT. +Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. +Definition countZmodType := @Zmodule.Pack cT xclass xT. +Definition ringType := @GRing.Ring.Pack cT xclass xT. +Definition countRingType := @Ring.Pack cT xclass xT. +Definition comRingType := @GRing.ComRing.Pack cT xclass xT. +Definition countComRingType := @ComRing.Pack cT xclass xT. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. +Definition countUnitRingType := @UnitRing.Pack cT xclass xT. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. +Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. +Definition countIdomainType := @IntegralDomain.Pack cT xclass xT. +Definition fieldType := @GRing.Field.Pack cT xclass xT. + +Definition join_countType := @Countable.Pack fieldType (cnt_ xclass) xT. +Definition join_countZmodType := @Zmodule.Pack fieldType xclass xT. +Definition join_countRingType := @Ring.Pack fieldType xclass xT. +Definition join_countUnitRingType := @UnitRing.Pack fieldType xclass xT. +Definition join_countComRingType := @ComRing.Pack fieldType xclass xT. +Definition join_countComUnitRingType := @ComUnitRing.Pack fieldType xclass xT. +Definition join_countIdomainType := @IntegralDomain.Pack fieldType xclass xT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> GRing.Field.class_of. +Coercion base2 : class_of >-> IntegralDomain.class_of. +Coercion sort : type >-> Sortclass. +Bind Scope ring_scope with sort. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical zmodType. +Coercion countZmodType : type >-> Zmodule.type. +Canonical countZmodType. +Coercion ringType : type >-> GRing.Ring.type. +Canonical ringType. +Coercion countRingType : type >-> Ring.type. +Canonical countRingType. +Coercion comRingType : type >-> GRing.ComRing.type. +Canonical comRingType. +Coercion countComRingType : type >-> ComRing.type. +Canonical countComRingType. +Coercion unitRingType : type >-> GRing.UnitRing.type. +Canonical unitRingType. +Coercion countUnitRingType : type >-> UnitRing.type. +Canonical countUnitRingType. +Coercion comUnitRingType : type >-> GRing.ComUnitRing.type. +Canonical comUnitRingType. +Coercion countComUnitRingType : type >-> ComUnitRing.type. +Canonical countComUnitRingType. +Coercion idomainType : type >-> GRing.IntegralDomain.type. +Canonical idomainType. +Coercion countIdomainType : type >-> IntegralDomain.type. +Canonical countIdomainType. +Coercion fieldType : type >-> GRing.Field.type. +Canonical fieldType. +Canonical join_countType. +Canonical join_countZmodType. +Canonical join_countRingType. +Canonical join_countComRingType. +Canonical join_countUnitRingType. +Canonical join_countComUnitRingType. +Canonical join_countIdomainType. +Notation countFieldType := CountRing.Field.type. +Notation "[ 'countFieldType' 'of' T ]" := (do_pack pack T) + (at level 0, format "[ 'countFieldType' 'of' T ]") : form_scope. +End Exports. + +End Field. +Import Field.Exports. + +Module DecidableField. + +Section ClassDef. + +Record class_of R := + Class { base : GRing.DecidableField.class_of R; mixin : mixin_of R }. +Definition base2 R (c : class_of R) := Field.Class (base c) (mixin c). +Local Coercion base : class_of >-> GRing.DecidableField.class_of. +Local Coercion base2 : class_of >-> Field.class_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Definition pack := gen_pack Pack Class GRing.DecidableField.class. +Variable cT : type. +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (cnt_ xclass) xT. +Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. +Definition countZmodType := @Zmodule.Pack cT xclass xT. +Definition ringType := @GRing.Ring.Pack cT xclass xT. +Definition countRingType := @Ring.Pack cT xclass xT. +Definition comRingType := @GRing.ComRing.Pack cT xclass xT. +Definition countComRingType := @ComRing.Pack cT xclass xT. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. +Definition countUnitRingType := @UnitRing.Pack cT xclass xT. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. +Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. +Definition countIdomainType := @IntegralDomain.Pack cT xclass xT. +Definition fieldType := @GRing.Field.Pack cT xclass xT. +Definition countFieldType := @Field.Pack cT xclass xT. +Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT. + +Definition join_countType := @Countable.Pack decFieldType (cnt_ xclass) xT. +Definition join_countZmodType := @Zmodule.Pack decFieldType xclass xT. +Definition join_countRingType := @Ring.Pack decFieldType xclass xT. +Definition join_countUnitRingType := @UnitRing.Pack decFieldType xclass xT. +Definition join_countComRingType := @ComRing.Pack decFieldType xclass xT. +Definition join_countComUnitRingType := + @ComUnitRing.Pack decFieldType xclass xT. +Definition join_countIdomainType := @IntegralDomain.Pack decFieldType xclass xT. +Definition join_countFieldType := @Field.Pack decFieldType xclass xT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> GRing.DecidableField.class_of. +Coercion base2 : class_of >-> Field.class_of. +Coercion sort : type >-> Sortclass. +Bind Scope ring_scope with sort. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical zmodType. +Coercion countZmodType : type >-> Zmodule.type. +Canonical countZmodType. +Coercion ringType : type >-> GRing.Ring.type. +Canonical ringType. +Coercion countRingType : type >-> Ring.type. +Canonical countRingType. +Coercion comRingType : type >-> GRing.ComRing.type. +Canonical comRingType. +Coercion countComRingType : type >-> ComRing.type. +Canonical countComRingType. +Coercion unitRingType : type >-> GRing.UnitRing.type. +Canonical unitRingType. +Coercion countUnitRingType : type >-> UnitRing.type. +Canonical countUnitRingType. +Coercion comUnitRingType : type >-> GRing.ComUnitRing.type. +Canonical comUnitRingType. +Coercion countComUnitRingType : type >-> ComUnitRing.type. +Canonical countComUnitRingType. +Coercion idomainType : type >-> GRing.IntegralDomain.type. +Canonical idomainType. +Coercion countIdomainType : type >-> IntegralDomain.type. +Canonical countIdomainType. +Coercion fieldType : type >-> GRing.Field.type. +Canonical fieldType. +Coercion countFieldType : type >-> Field.type. +Canonical countFieldType. +Coercion decFieldType : type >-> GRing.DecidableField.type. +Canonical decFieldType. +Canonical join_countType. +Canonical join_countZmodType. +Canonical join_countRingType. +Canonical join_countComRingType. +Canonical join_countUnitRingType. +Canonical join_countComUnitRingType. +Canonical join_countIdomainType. +Canonical join_countFieldType. +Notation countDecFieldType := CountRing.DecidableField.type. +Notation "[ 'countDecFieldType' 'of' T ]" := (do_pack pack T) + (at level 0, format "[ 'countDecFieldType' 'of' T ]") : form_scope. +End Exports. + +End DecidableField. +Import DecidableField.Exports. + +Module ClosedField. + +Section ClassDef. + +Record class_of R := + Class { base : GRing.ClosedField.class_of R; mixin : mixin_of R }. +Definition base2 R (c : class_of R) := DecidableField.Class (base c) (mixin c). +Local Coercion base : class_of >-> GRing.ClosedField.class_of. +Local Coercion base2 : class_of >-> DecidableField.class_of. + +Structure type := Pack {sort; _ : class_of sort; _ : Type}. +Local Coercion sort : type >-> Sortclass. +Definition pack := gen_pack Pack Class GRing.ClosedField.class. +Variable cT : type. +Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. +Let xT := let: Pack T _ _ := cT in T. +Notation xclass := (class : class_of xT). + +Definition eqType := @Equality.Pack cT xclass xT. +Definition choiceType := @Choice.Pack cT xclass xT. +Definition countType := @Countable.Pack cT (cnt_ xclass) xT. +Definition zmodType := @GRing.Zmodule.Pack cT xclass xT. +Definition countZmodType := @Zmodule.Pack cT xclass xT. +Definition ringType := @GRing.Ring.Pack cT xclass xT. +Definition countRingType := @Ring.Pack cT xclass xT. +Definition comRingType := @GRing.ComRing.Pack cT xclass xT. +Definition countComRingType := @ComRing.Pack cT xclass xT. +Definition unitRingType := @GRing.UnitRing.Pack cT xclass xT. +Definition countUnitRingType := @UnitRing.Pack cT xclass xT. +Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass xT. +Definition countComUnitRingType := @ComUnitRing.Pack cT xclass xT. +Definition idomainType := @GRing.IntegralDomain.Pack cT xclass xT. +Definition countIdomainType := @IntegralDomain.Pack cT xclass xT. +Definition fieldType := @GRing.Field.Pack cT xclass xT. +Definition countFieldType := @Field.Pack cT xclass xT. +Definition decFieldType := @GRing.DecidableField.Pack cT xclass xT. +Definition countDecFieldType := @DecidableField.Pack cT xclass xT. +Definition closedFieldType := @GRing.ClosedField.Pack cT xclass xT. + +Definition join_countType := @Countable.Pack closedFieldType (cnt_ xclass) xT. +Definition join_countZmodType := @Zmodule.Pack closedFieldType xclass xT. +Definition join_countRingType := @Ring.Pack closedFieldType xclass xT. +Definition join_countUnitRingType := @UnitRing.Pack closedFieldType xclass xT. +Definition join_countComRingType := @ComRing.Pack closedFieldType xclass xT. +Definition join_countComUnitRingType := + @ComUnitRing.Pack closedFieldType xclass xT. +Definition join_countIdomainType := + @IntegralDomain.Pack closedFieldType xclass xT. +Definition join_countFieldType := @Field.Pack closedFieldType xclass xT. +Definition join_countDecFieldType := + @DecidableField.Pack closedFieldType xclass xT. + +End ClassDef. + +Module Exports. +Coercion base : class_of >-> GRing.ClosedField.class_of. +Coercion base2 : class_of >-> DecidableField.class_of. +Coercion sort : type >-> Sortclass. +Bind Scope ring_scope with sort. +Coercion eqType : type >-> Equality.type. +Canonical eqType. +Coercion choiceType : type >-> Choice.type. +Canonical choiceType. +Coercion countType : type >-> Countable.type. +Canonical countType. +Coercion zmodType : type >-> GRing.Zmodule.type. +Canonical zmodType. +Coercion countZmodType : type >-> Zmodule.type. +Canonical countZmodType. +Coercion ringType : type >-> GRing.Ring.type. +Canonical ringType. +Coercion countRingType : type >-> Ring.type. +Canonical countRingType. +Coercion comRingType : type >-> GRing.ComRing.type. +Canonical comRingType. +Coercion countComRingType : type >-> ComRing.type. +Canonical countComRingType. +Coercion unitRingType : type >-> GRing.UnitRing.type. +Canonical unitRingType. +Coercion countUnitRingType : type >-> UnitRing.type. +Canonical countUnitRingType. +Coercion comUnitRingType : type >-> GRing.ComUnitRing.type. +Canonical comUnitRingType. +Coercion countComUnitRingType : type >-> ComUnitRing.type. +Canonical countComUnitRingType. +Coercion idomainType : type >-> GRing.IntegralDomain.type. +Canonical idomainType. +Coercion fieldType : type >-> GRing.Field.type. +Canonical fieldType. +Coercion countFieldType : type >-> Field.type. +Canonical countFieldType. +Coercion decFieldType : type >-> GRing.DecidableField.type. +Canonical decFieldType. +Coercion countDecFieldType : type >-> DecidableField.type. +Canonical countDecFieldType. +Coercion closedFieldType : type >-> GRing.ClosedField.type. +Canonical closedFieldType. +Canonical join_countType. +Canonical join_countZmodType. +Canonical join_countRingType. +Canonical join_countComRingType. +Canonical join_countUnitRingType. +Canonical join_countComUnitRingType. +Canonical join_countIdomainType. +Canonical join_countFieldType. +Canonical join_countDecFieldType. +Notation countClosedFieldType := CountRing.ClosedField.type. +Notation "[ 'countClosedFieldType' 'of' T ]" := (do_pack pack T) + (at level 0, format "[ 'countClosedFieldType' 'of' T ]") : form_scope. +End Exports. + +End ClosedField. +Import ClosedField.Exports. + +End CountRing. + +Import CountRing. +Export Zmodule.Exports Ring.Exports ComRing.Exports UnitRing.Exports. +Export ComUnitRing.Exports IntegralDomain.Exports. +Export Field.Exports DecidableField.Exports ClosedField.Exports.
\ No newline at end of file diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index 7a1cacf..939cd38 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. From mathcomp -Require Import ssralg finset fingroup morphism perm action. +Require Import ssralg finset fingroup morphism perm action countalg. (*****************************************************************************) (* This file clones the entire ssralg hierachy for finite types; this allows *) @@ -136,6 +136,7 @@ Notation "[ 'baseFinGroupType' 'of' R 'for' +%R ]" := Notation "[ 'finGroupType' 'of' R 'for' +%R ]" := (@FinGroup.clone R _ (finGroupType _) id _ id) (at level 0, format "[ 'finGroupType' 'of' R 'for' +%R ]") : form_scope. +Canonical countZmodType (T : type) := [countZmodType of T]. End Exports. End Zmodule. @@ -219,6 +220,8 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. End Exports. Section Unit. @@ -330,6 +333,9 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countComRingType (T : type) := [countComRingType of T]. End Exports. End ComRing. @@ -407,6 +413,9 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countUnitRingType (T : type) := [countUnitRingType of T]. End Exports. End UnitRing. @@ -590,6 +599,11 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countUnitRingType (T : type) := [countUnitRingType of T]. +Canonical countComRingType (T : type) := [countComRingType of T]. +Canonical countComUnitRingType (T : type) := [countComUnitRingType of T]. End Exports. End ComUnitRing. @@ -691,6 +705,12 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countUnitRingType (T : type) := [countUnitRingType of T]. +Canonical countComRingType (T : type) := [countComRingType of T]. +Canonical countComUnitRingType (T : type) := [countComUnitRingType of T]. +Canonical countIdomainType (T : type) := [countIdomainType of T]. End Exports. End IntegralDomain. @@ -800,6 +820,13 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Canonical countZmodType (T : type) := [countZmodType of T]. +Canonical countRingType (T : type) := [countRingType of T]. +Canonical countUnitRingType (T : type) := [countUnitRingType of T]. +Canonical countComRingType (T : type) := [countComRingType of T]. +Canonical countComUnitRingType (T : type) := [countComUnitRingType of T]. +Canonical countIdomainType (T : type) := [countIdomainType of T]. +Canonical countFieldType (T : type) := [countFieldType of T]. End Exports. End Field. @@ -871,6 +898,7 @@ Canonical finComUnitRingType. Canonical finIdomainType. Canonical baseFinGroupType. Canonical finGroupType. + End Exports. End DecField. @@ -940,6 +968,10 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Section counttype. +Variables (R : ringType) (phR : phant R) (T : type phR). +Canonical countZmodType := [countZmodType of T]. +End counttype. End Exports. End Lmodule. @@ -1036,6 +1068,11 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Section counttype. +Variables (R : GRing.Ring.type) (phR : phant R) (T : type phR). +Canonical countZmodType := [countZmodType of T]. +Canonical countRingType := [countRingType of T]. +End counttype. End Exports. End Lalgebra. @@ -1131,18 +1168,23 @@ Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Section counttype. +Variables (R : GRing.Ring.type) (phR : phant R) (T : type phR). +Canonical countZmodType := [countZmodType of T]. +Canonical countRingType := [countRingType of T]. +End counttype. End Exports. End Algebra. Import Algebra.Exports. Module UnitAlgebra. - + Section ClassDef. Variable R : unitRingType. - -Record class_of M := + +Record class_of M := Class { base : GRing.UnitAlgebra.class_of R M; mixin : mixin_of M base }. Definition base2 M (c : class_of M) := Algebra.Class (mixin c). Definition base3 M (c : class_of M) := @UnitRing.Class _ (base c) (mixin c). @@ -1257,12 +1299,18 @@ Canonical ujoin_finLmodType. Canonical ujoin_finLalgType. Canonical ujoin_finAlgType. Notation finUnitAlgType R := (type (Phant R)). -Notation "[ 'finUnitAlgType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T) +Notation "[ 'finUnitAlgType' R 'of' T ]" := (do_pack (@pack _ (Phant R)) T) (at level 0, format "[ 'finUnitAlgType' R 'of' T ]") : form_scope. Canonical baseFinGroupType. Canonical finGroupType. Canonical join_baseFinGroupType. Canonical join_finGroupType. +Section counttype. +Variables (R : GRing.UnitRing.type) (phR : phant R) (T : type phR). +Canonical countZmodType := [countZmodType of T]. +Canonical countRingType := [countRingType of T]. +Canonical countUnitRingType := [countUnitRingType of T]. +End counttype. End Exports. End UnitAlgebra. @@ -1297,4 +1345,3 @@ Notation "{ 'unit' R }" := (unit_of (Phant R)) Prenex Implicits FinRing.uval. Notation "''U'" := (unit_action _) (at level 8) : action_scope. Notation "''U'" := (unit_groupAction _) (at level 8) : groupAction_scope. - diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index fca25a9..2a701a2 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -6,7 +6,7 @@ Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. From mathcomp Require Import finfun bigop prime binomial ssralg finset fingroup finalg. From mathcomp -Require Import perm zmodp. +Require Import perm zmodp countalg. (******************************************************************************) (* Basic concrete linear algebra : definition of type for matrices, and all *) @@ -2071,6 +2071,10 @@ Proof. by apply/matrixP=> k i; rewrite !mxE; apply: eq_bigr => j _; rewrite !mxE. Qed. +Canonical matrix_countZmodType (M : countZmodType) m n := + [countZmodType of 'M[M]_(m, n)]. +Canonical matrix_countRingType (R : countRingType) n := + [countRingType of 'M[R]_n.+1]. Canonical matrix_finLmodType (R : finRingType) m n := [finLmodType R of 'M[R]_(m, n)]. Canonical matrix_finRingType (R : finRingType) n' := @@ -2644,6 +2648,9 @@ End MatrixInv. Prenex Implicits unitmx invmx. +Canonical matrix_countUnitRingType (R : countComUnitRingType) n := + [countUnitRingType of 'M[R]_n.+1]. + (* Finite inversible matrices and the general linear group. *) Section FinUnitMatrix. diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index 0f97bb0..040b3a8 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. From mathcomp -Require Import bigop ssralg binomial tuple. +Require Import bigop ssralg countalg binomial tuple. (******************************************************************************) (* This file provides a library for univariate polynomials over ring *) @@ -152,6 +152,11 @@ Arguments coefp_head _ _ _%N _%R. Notation "{ 'poly' T }" := (poly_of (Phant T)). Notation coefp i := (coefp_head tt i). +Definition poly_countMixin (R : countRingType) := + [countMixin of polynomial R by <:]. +Canonical polynomial_countType R := CountType _ (poly_countMixin R). +Canonical poly_countType (R : countRingType) := [countType of {poly R}]. + Section PolynomialTheory. Variable R : ringType. @@ -1690,6 +1695,13 @@ Arguments rootPt [R p x]. Arguments unity_rootP [R n z]. Arguments polyOverP {R S0 addS kS p}. +Canonical polynomial_countZmodType (R : countRingType) := + [countZmodType of polynomial R]. +Canonical poly_countZmodType (R : countRingType) := [countZmodType of {poly R}]. +Canonical polynomial_countRingType (R : countRingType) := + [countRingType of polynomial R]. +Canonical poly_countRingType (R : countRingType) := [countRingType of {poly R}]. + (* Container morphism. *) Section MapPoly. @@ -2116,6 +2128,11 @@ Definition derivCE := (derivE, deriv_exp). End PolynomialComRing. +Canonical polynomial_countComRingType (R : countComRingType) := + [countComRingType of polynomial R]. +Canonical poly_countComRingType (R : countComRingType) := + [countComRingType of {poly R}]. + Section PolynomialIdomain. (* Integral domain structure on poly *) @@ -2353,6 +2370,19 @@ Proof. by move=> ??; apply: contraTeq => ?; rewrite leqNgt max_poly_roots. Qed. End PolynomialIdomain. +Canonical polynomial_countUnitRingType (R : countIdomainType) := + [countUnitRingType of polynomial R]. +Canonical poly_countUnitRingType (R : countIdomainType) := + [countUnitRingType of {poly R}]. +Canonical polynomial_countComUnitRingType (R : countIdomainType) := + [countComUnitRingType of polynomial R]. +Canonical poly_countComUnitRingType (R : countIdomainType) := + [countComUnitRingType of {poly R}]. +Canonical polynomial_countIdomainType (R : countIdomainType) := + [countIdomainType of polynomial R]. +Canonical poly_countIdomainType (R : countIdomainType) := + [countIdomainType of {poly R}]. + Section MapFieldPoly. Variables (F : fieldType) (R : ringType) (f : {rmorphism F -> R}). diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index b56bc2a..6015f33 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype. From mathcomp -Require Import bigop ssralg div ssrnum ssrint. +Require Import bigop ssralg countalg div ssrnum ssrint. (******************************************************************************) (* This file defines a datatype for rational numbers and equips it with a *) @@ -350,6 +350,14 @@ Canonical rat_iDomain := Eval hnf in IdomainType rat (FieldIdomainMixin rat_field_axiom). Canonical rat_fieldType := FieldType rat rat_field_axiom. +Canonical rat_countZmodType := [countZmodType of rat]. +Canonical rat_countRingType := [countRingType of rat]. +Canonical rat_countComRingType := [countComRingType of rat]. +Canonical rat_countUnitRingType := [countUnitRingType of rat]. +Canonical rat_countComUnitRingType := [countComUnitRingType of rat]. +Canonical rat_countIdomainType := [countIdomainType of rat]. +Canonical rat_countFieldType := [countFieldType of rat]. + Lemma numq_eq0 x : (numq x == 0) = (x == 0). Proof. rewrite -[x]valqK fracq_eq0; case: fracqP=> /= [|k {x} x k0]. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index f12784b..d0214dd 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat choice seq. From mathcomp -Require Import fintype finfun bigop ssralg ssrnum poly. +Require Import fintype finfun bigop ssralg countalg ssrnum poly. Import GRing.Theory Num.Theory. (******************************************************************************) @@ -359,6 +359,13 @@ Canonical int_comUnitRing := Eval hnf in [comUnitRingType of int]. Canonical int_iDomain := Eval hnf in IdomainType int intUnitRing.idomain_axiomz. +Canonical int_countZmodType := [countZmodType of int]. +Canonical int_countRingType := [countRingType of int]. +Canonical int_countComRingType := [countComRingType of int]. +Canonical int_countUnitRingType := [countUnitRingType of int]. +Canonical int_countComUnitRingType := [countComUnitRingType of int]. +Canonical int_countIdomainType := [countIdomainType of int]. + Definition absz m := match m with Posz p => p | Negz n => n.+1 end. Notation "m - n" := (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope. diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index f9bdaaa..ba6c1b3 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -4,7 +4,7 @@ Require Import mathcomp.ssreflect.ssreflect. From mathcomp Require Import ssrfun ssrbool eqtype ssrnat seq div. From mathcomp -Require Import fintype bigop finset prime fingroup ssralg finalg. +Require Import fintype bigop finset prime fingroup ssralg finalg countalg. (******************************************************************************) (* Definition of the additive group and ring Zp, represented as 'I_p *) @@ -364,3 +364,12 @@ Canonical Fp_decFieldType := Eval hnf in [decFieldType of 'F_p for Fp_finFieldType]. End PrimeField. + +Canonical Zp_countZmodType m := [countZmodType of 'I_m.+1]. +Canonical Zp_countRingType m := [countRingType of 'I_m.+2]. +Canonical Zp_countComRingType m := [countComRingType of 'I_m.+2]. +Canonical Zp_countUnitRingType m := [countUnitRingType of 'I_m.+2]. +Canonical Zp_countComUnitRingType m := [countComUnitRingType of 'I_m.+2]. +Canonical Fp_countIdomainType p := [countIdomainType of 'F_p]. +Canonical Fp_countFieldType p := [countFieldType of 'F_p]. +Canonical Fp_countDecFieldType p := [countDecFieldType of 'F_p]. |