Library mathcomp.field.countalg
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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.
+ +
+Local Open Scope ring_scope.
+Import GRing.Theory CodeSeq.
+ +
+Module CountRing.
+ +
+ +
+Section Generic.
+ +
+
+
++Set Implicit Arguments.
+ +
+Local Open Scope ring_scope.
+Import GRing.Theory CodeSeq.
+ +
+Module CountRing.
+ +
+ +
+Section Generic.
+ +
+
+ Implicits
+
+
+Variables (type base_type : Type) (class_of base_of : Type → Type).
+Variable base_sort : base_type → Type.
+ +
+
+
++Variable base_sort : base_type → Type.
+ +
+
+ Explicits
+
+
+Variable Pack : ∀ T, class_of T → Type → type.
+Variable Class : ∀ T, base_of T → mixin_of T → 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 c m & phant_id (Countable.class fT) (Countable.Class c m) ⇒
+ Pack (@Class T b m) T.
+ +
+End Generic.
+ +
+Import GRing.Theory.
+ +
+Module Zmodule.
+ +
+Section ClassDef.
+ +
+Record class_of M :=
+ Class { base : GRing.Zmodule.class_of M; mixin : mixin_of M }.
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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.
+ +
+Import GRing.Theory.
+ +
+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].
+ +
+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_countUnitRingType (R : countComUnitRingType) n :=
+ [countUnitRingType of 'M[R]_n.+1].
+ +
+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}].
+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}].
+Canonical polynomial_countComRingType (R : countComRingType) :=
+ [countComRingType of polynomial R].
+Canonical poly_countComRingType (R : countComRingType) :=
+ [countComRingType of {poly R}].
+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}].
+ +
+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].
+ +
+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 countable_field_extension (F : countFieldType) (p : {poly F}) :
+ size p > 1 →
+ {E : countFieldType & {FtoE : {rmorphism F → E} &
+ {w : E | root (map_poly FtoE p) w
+ & ∀ u : E, ∃ q, u = (map_poly FtoE q).[w]}}}.
+ +
+Lemma countable_algebraic_closure (F : countFieldType) :
+ {K : countClosedFieldType & {FtoK : {rmorphism F → K} | integralRange FtoK}}.
+
++Variable Class : ∀ T, base_of T → mixin_of T → 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 c m & phant_id (Countable.class fT) (Countable.Class c m) ⇒
+ Pack (@Class T b m) T.
+ +
+End Generic.
+ +
+Import GRing.Theory.
+ +
+Module Zmodule.
+ +
+Section ClassDef.
+ +
+Record class_of M :=
+ Class { base : GRing.Zmodule.class_of M; mixin : mixin_of M }.
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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).
+ +
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+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.
+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.
+ +
+Import GRing.Theory.
+ +
+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].
+ +
+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_countUnitRingType (R : countComUnitRingType) n :=
+ [countUnitRingType of 'M[R]_n.+1].
+ +
+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}].
+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}].
+Canonical polynomial_countComRingType (R : countComRingType) :=
+ [countComRingType of polynomial R].
+Canonical poly_countComRingType (R : countComRingType) :=
+ [countComRingType of {poly R}].
+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}].
+ +
+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].
+ +
+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 countable_field_extension (F : countFieldType) (p : {poly F}) :
+ size p > 1 →
+ {E : countFieldType & {FtoE : {rmorphism F → E} &
+ {w : E | root (map_poly FtoE p) w
+ & ∀ u : E, ∃ q, u = (map_poly FtoE q).[w]}}}.
+ +
+Lemma countable_algebraic_closure (F : countFieldType) :
+ {K : countClosedFieldType & {FtoK : {rmorphism F → K} | integralRange FtoK}}.
+