- -

Library mathcomp.field.countalg

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- 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.
- -
-

- -

- Implicits -

-Variables (type base_type : Type) (class_of base_of : 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 }}.
-