Library mathcomp.field.countalg

(* (c) Copyright 2006-2015 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.

Implicit Arguments gen_pack [type base_type class_of base_of base_sort].
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}}.