Library mathcomp.field.finfield
+ +
+(* (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.
+ +
+
+ Additional constructions and results on finite fields.
+
+
+
+ FinFieldExtType L == A FinFieldType structure on the carrier of L,
+ where L IS a fieldExtType F structure for an
+ F that has a finFieldType structure. This
+ does not take any existing finType structure
+ on L; this should not be made canonical.
+ FinSplittingFieldType F L == A SplittingFieldType F structure on the
+ carrier of L, where L IS a fieldExtType F for
+ an F with a finFieldType structure; this
+ should not be made canonical.
+ Import FinVector :: Declares canonical default finType, finRing,
+ etc structures (including FinFieldExtType
+ above) for abstract vectType, FalgType and
+ fieldExtType over a finFieldType. This should
+ be used with caution (e.g., local to a proof)
+ as the finType so obtained may clash with the
+ canonical one for standard types like matrix.
+ PrimeCharType charRp == The carrier of a ringType R such that
+ charRp : p \in [char R] holds. This type has
+ canonical ringType, ..., fieldType structures
+ compatible with those of R, as well as
+ canonical lmodType 'F_p, ..., algType 'F_p
+ structures, plus an FalgType structure if R
+ is a finUnitRingType and a splittingFieldType
+ struture if R is a finFieldType.
+ FinSplittingFieldFor nz_p == sigma-pair whose sval is a splittingFieldType
+ that is the splitting field for p : {poly F}
+ over F : finFieldType, given nz_p : p != 0.
+ PrimePowerField pr_p k_gt0 == sigma2-triple whose s2val is a finFieldType
+ of characteristic p and order m = p ^ k,
+ given pr_p : prime p and k_gt0 : k > 0.
+ FinDomainFieldType domR == A finFieldType structure on a finUnitRingType
+ R, given domR : GRing.IntegralDomain.axiom R.
+ This is intended to be used inside proofs,
+ where one cannot declare Canonical instances.
+ Otherwise one should construct explicitly the
+ intermediate structures using the ssralg and
+ finalg constructors, and finDomain_mulrC domR
+ finDomain_fieldP domR to prove commutativity
+ and field axioms (the former is Wedderburn's
+ little theorem).
+ FinDomainSplittingFieldType domR charRp == A splittingFieldType structure
+ that repackages the two constructions above.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory FinRing.Theory.
+Local Open Scope ring_scope.
+ +
+Section FinRing.
+ +
+Variable R : finRingType.
+ +
+Lemma finRing_nontrivial : [set: R] != 1%g.
+ +
+Lemma finRing_gt1 : 1 < #|R|.
+ +
+End FinRing.
+ +
+Section FinField.
+ +
+Variable F : finFieldType.
+ +
+Lemma card_finField_unit : #|[set: {unit F}]| = #|F|.-1.
+ +
+Definition finField_unit x (nz_x : x != 0) :=
+ FinRing.unit F (etrans (unitfE x) nz_x).
+ +
+Lemma expf_card x : x ^+ #|F| = x :> F.
+ +
+Lemma finField_genPoly : 'X^#|F| - 'X = \prod_x ('X - x%:P) :> {poly F}.
+ +
+Lemma finCharP : {p | prime p & p \in [char F]}.
+ +
+Lemma finField_is_abelem : is_abelem [set: F].
+ +
+Lemma card_finCharP p n : #|F| = (p ^ n)%N → prime p → p \in [char F].
+ +
+End FinField.
+ +
+Section CardVspace.
+ +
+Variables (F : finFieldType) (T : finType).
+ +
+Section Vector.
+ +
+Variable cvT : Vector.class_of F T.
+Let vT := Vector.Pack (Phant F) cvT T.
+ +
+Lemma card_vspace (V : {vspace vT}) : #|V| = (#|F| ^ \dim V)%N.
+ +
+Lemma card_vspacef : #|{: vT}%VS| = #|T|.
+ +
+End Vector.
+ +
+Variable caT : Falgebra.class_of F T.
+Let aT := Falgebra.Pack (Phant F) caT T.
+ +
+Lemma card_vspace1 : #|(1%VS : {vspace aT})| = #|F|.
+ +
+End CardVspace.
+ +
+Lemma VectFinMixin (R : finRingType) (vT : vectType R) : Finite.mixin_of vT.
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GroupScope GRing.Theory FinRing.Theory.
+Local Open Scope ring_scope.
+ +
+Section FinRing.
+ +
+Variable R : finRingType.
+ +
+Lemma finRing_nontrivial : [set: R] != 1%g.
+ +
+Lemma finRing_gt1 : 1 < #|R|.
+ +
+End FinRing.
+ +
+Section FinField.
+ +
+Variable F : finFieldType.
+ +
+Lemma card_finField_unit : #|[set: {unit F}]| = #|F|.-1.
+ +
+Definition finField_unit x (nz_x : x != 0) :=
+ FinRing.unit F (etrans (unitfE x) nz_x).
+ +
+Lemma expf_card x : x ^+ #|F| = x :> F.
+ +
+Lemma finField_genPoly : 'X^#|F| - 'X = \prod_x ('X - x%:P) :> {poly F}.
+ +
+Lemma finCharP : {p | prime p & p \in [char F]}.
+ +
+Lemma finField_is_abelem : is_abelem [set: F].
+ +
+Lemma card_finCharP p n : #|F| = (p ^ n)%N → prime p → p \in [char F].
+ +
+End FinField.
+ +
+Section CardVspace.
+ +
+Variables (F : finFieldType) (T : finType).
+ +
+Section Vector.
+ +
+Variable cvT : Vector.class_of F T.
+Let vT := Vector.Pack (Phant F) cvT T.
+ +
+Lemma card_vspace (V : {vspace vT}) : #|V| = (#|F| ^ \dim V)%N.
+ +
+Lemma card_vspacef : #|{: vT}%VS| = #|T|.
+ +
+End Vector.
+ +
+Variable caT : Falgebra.class_of F T.
+Let aT := Falgebra.Pack (Phant F) caT T.
+ +
+Lemma card_vspace1 : #|(1%VS : {vspace aT})| = #|F|.
+ +
+End CardVspace.
+ +
+Lemma VectFinMixin (R : finRingType) (vT : vectType R) : Finite.mixin_of vT.
+ +
+
+ These instancces are not exported by default because they conflict with
+ existing finType instances such as matrix_finType or primeChar_finType.
+
+
+Module FinVector.
+Section Interfaces.
+ +
+Variable F : finFieldType.
+Implicit Types (vT : vectType F) (aT : FalgType F) (fT : fieldExtType F).
+ +
+Canonical vect_finType vT := FinType vT (VectFinMixin vT).
+Canonical Falg_finType aT := FinType aT (VectFinMixin aT).
+Canonical fieldExt_finType fT := FinType fT (VectFinMixin fT).
+ +
+Canonical Falg_finRingType aT := [finRingType of aT].
+Canonical fieldExt_finRingType fT := [finRingType of fT].
+Canonical fieldExt_finFieldType fT := [finFieldType of fT].
+ +
+Lemma finField_splittingField_axiom fT : SplittingField.axiom fT.
+ +
+End Interfaces.
+End FinVector.
+ +
+Notation FinFieldExtType := FinVector.fieldExt_finFieldType.
+Notation FinSplittingFieldAxiom := (FinVector.finField_splittingField_axiom _).
+Notation FinSplittingFieldType F L :=
+ (SplittingFieldType F L FinSplittingFieldAxiom).
+ +
+Section PrimeChar.
+ +
+Variable p : nat.
+ +
+Section PrimeCharRing.
+ +
+Variable R0 : ringType.
+ +
+Definition PrimeCharType of p \in [char R0] : predArgType := R0.
+ +
+Hypothesis charRp : p \in [char R0].
+Implicit Types (a b : 'F_p) (x y : R).
+ +
+Canonical primeChar_eqType := [eqType of R].
+Canonical primeChar_choiceType := [choiceType of R].
+Canonical primeChar_zmodType := [zmodType of R].
+Canonical primeChar_ringType := [ringType of R].
+ +
+Definition primeChar_scale a x := a%:R × x.
+ +
+Let natrFp n : (inZp n : 'F_p)%:R = n%:R :> R.
+ +
+Lemma primeChar_scaleA a b x : a ×p: (b ×p: x) = (a × b) ×p: x.
+ +
+Lemma primeChar_scale1 : left_id 1 primeChar_scale.
+ +
+Lemma primeChar_scaleDr : right_distributive primeChar_scale +%R.
+ +
+Lemma primeChar_scaleDl x : {morph primeChar_scale^~ x: a b / a + b}.
+ +
+Definition primeChar_lmodMixin :=
+ LmodMixin primeChar_scaleA primeChar_scale1
+ primeChar_scaleDr primeChar_scaleDl.
+Canonical primeChar_lmodType := LmodType 'F_p R primeChar_lmodMixin.
+ +
+Lemma primeChar_scaleAl : GRing.Lalgebra.axiom ( *%R : R → R → R).
+ Canonical primeChar_LalgType := LalgType 'F_p R primeChar_scaleAl.
+ +
+Lemma primeChar_scaleAr : GRing.Algebra.axiom primeChar_LalgType.
+ Canonical primeChar_algType := AlgType 'F_p R primeChar_scaleAr.
+ +
+End PrimeCharRing.
+ +
+ +
+Canonical primeChar_unitRingType (R : unitRingType) charRp :=
+ [unitRingType of type R charRp].
+Canonical primeChar_unitAlgType (R : unitRingType) charRp :=
+ [unitAlgType 'F_p of type R charRp].
+Canonical primeChar_comRingType (R : comRingType) charRp :=
+ [comRingType of type R charRp].
+Canonical primeChar_comUnitRingType (R : comUnitRingType) charRp :=
+ [comUnitRingType of type R charRp].
+Canonical primeChar_idomainType (R : idomainType) charRp :=
+ [idomainType of type R charRp].
+Canonical primeChar_fieldType (F : fieldType) charFp :=
+ [fieldType of type F charFp].
+ +
+Section FinRing.
+ +
+Variables (R0 : finRingType) (charRp : p \in [char R0]).
+ +
+Canonical primeChar_finType := [finType of R].
+Canonical primeChar_finZmodType := [finZmodType of R].
+Canonical primeChar_baseGroupType := [baseFinGroupType of R for +%R].
+Canonical primeChar_groupType := [finGroupType of R for +%R].
+Canonical primeChar_finRingType := [finRingType of R].
+Canonical primeChar_finLmodType := [finLmodType 'F_p of R].
+Canonical primeChar_finLalgType := [finLalgType 'F_p of R].
+Canonical primeChar_finAlgType := [finAlgType 'F_p of R].
+ +
+Let pr_p : prime p.
+ +
+Lemma primeChar_abelem : p.-abelem [set: R].
+ +
+Lemma primeChar_pgroup : p.-group [set: R].
+ +
+Lemma order_primeChar x : x != 0 :> R → #[x]%g = p.
+ +
+Let n := logn p #|R|.
+ +
+Lemma card_primeChar : #|R| = (p ^ n)%N.
+ +
+Lemma primeChar_vectAxiom : Vector.axiom n (primeChar_lmodType charRp).
+ +
+Definition primeChar_vectMixin := Vector.Mixin primeChar_vectAxiom.
+Canonical primeChar_vectType := VectType 'F_p R primeChar_vectMixin.
+ +
+Lemma primeChar_dimf : \dim {:primeChar_vectType} = n.
+ +
+End FinRing.
+ +
+Canonical primeChar_finUnitRingType (R : finUnitRingType) charRp :=
+ [finUnitRingType of type R charRp].
+Canonical primeChar_finUnitAlgType (R : finUnitRingType) charRp :=
+ [finUnitAlgType 'F_p of type R charRp].
+Canonical primeChar_FalgType (R : finUnitRingType) charRp :=
+ [FalgType 'F_p of type R charRp].
+Canonical primeChar_finComRingType (R : finComRingType) charRp :=
+ [finComRingType of type R charRp].
+Canonical primeChar_finComUnitRingType (R : finComUnitRingType) charRp :=
+ [finComUnitRingType of type R charRp].
+Canonical primeChar_finIdomainType (R : finIdomainType) charRp :=
+ [finIdomainType of type R charRp].
+ +
+Section FinField.
+ +
+Variables (F0 : finFieldType) (charFp : p \in [char F0]).
+ +
+Canonical primeChar_finFieldType := [finFieldType of F].
+
+
++Section Interfaces.
+ +
+Variable F : finFieldType.
+Implicit Types (vT : vectType F) (aT : FalgType F) (fT : fieldExtType F).
+ +
+Canonical vect_finType vT := FinType vT (VectFinMixin vT).
+Canonical Falg_finType aT := FinType aT (VectFinMixin aT).
+Canonical fieldExt_finType fT := FinType fT (VectFinMixin fT).
+ +
+Canonical Falg_finRingType aT := [finRingType of aT].
+Canonical fieldExt_finRingType fT := [finRingType of fT].
+Canonical fieldExt_finFieldType fT := [finFieldType of fT].
+ +
+Lemma finField_splittingField_axiom fT : SplittingField.axiom fT.
+ +
+End Interfaces.
+End FinVector.
+ +
+Notation FinFieldExtType := FinVector.fieldExt_finFieldType.
+Notation FinSplittingFieldAxiom := (FinVector.finField_splittingField_axiom _).
+Notation FinSplittingFieldType F L :=
+ (SplittingFieldType F L FinSplittingFieldAxiom).
+ +
+Section PrimeChar.
+ +
+Variable p : nat.
+ +
+Section PrimeCharRing.
+ +
+Variable R0 : ringType.
+ +
+Definition PrimeCharType of p \in [char R0] : predArgType := R0.
+ +
+Hypothesis charRp : p \in [char R0].
+Implicit Types (a b : 'F_p) (x y : R).
+ +
+Canonical primeChar_eqType := [eqType of R].
+Canonical primeChar_choiceType := [choiceType of R].
+Canonical primeChar_zmodType := [zmodType of R].
+Canonical primeChar_ringType := [ringType of R].
+ +
+Definition primeChar_scale a x := a%:R × x.
+ +
+Let natrFp n : (inZp n : 'F_p)%:R = n%:R :> R.
+ +
+Lemma primeChar_scaleA a b x : a ×p: (b ×p: x) = (a × b) ×p: x.
+ +
+Lemma primeChar_scale1 : left_id 1 primeChar_scale.
+ +
+Lemma primeChar_scaleDr : right_distributive primeChar_scale +%R.
+ +
+Lemma primeChar_scaleDl x : {morph primeChar_scale^~ x: a b / a + b}.
+ +
+Definition primeChar_lmodMixin :=
+ LmodMixin primeChar_scaleA primeChar_scale1
+ primeChar_scaleDr primeChar_scaleDl.
+Canonical primeChar_lmodType := LmodType 'F_p R primeChar_lmodMixin.
+ +
+Lemma primeChar_scaleAl : GRing.Lalgebra.axiom ( *%R : R → R → R).
+ Canonical primeChar_LalgType := LalgType 'F_p R primeChar_scaleAl.
+ +
+Lemma primeChar_scaleAr : GRing.Algebra.axiom primeChar_LalgType.
+ Canonical primeChar_algType := AlgType 'F_p R primeChar_scaleAr.
+ +
+End PrimeCharRing.
+ +
+ +
+Canonical primeChar_unitRingType (R : unitRingType) charRp :=
+ [unitRingType of type R charRp].
+Canonical primeChar_unitAlgType (R : unitRingType) charRp :=
+ [unitAlgType 'F_p of type R charRp].
+Canonical primeChar_comRingType (R : comRingType) charRp :=
+ [comRingType of type R charRp].
+Canonical primeChar_comUnitRingType (R : comUnitRingType) charRp :=
+ [comUnitRingType of type R charRp].
+Canonical primeChar_idomainType (R : idomainType) charRp :=
+ [idomainType of type R charRp].
+Canonical primeChar_fieldType (F : fieldType) charFp :=
+ [fieldType of type F charFp].
+ +
+Section FinRing.
+ +
+Variables (R0 : finRingType) (charRp : p \in [char R0]).
+ +
+Canonical primeChar_finType := [finType of R].
+Canonical primeChar_finZmodType := [finZmodType of R].
+Canonical primeChar_baseGroupType := [baseFinGroupType of R for +%R].
+Canonical primeChar_groupType := [finGroupType of R for +%R].
+Canonical primeChar_finRingType := [finRingType of R].
+Canonical primeChar_finLmodType := [finLmodType 'F_p of R].
+Canonical primeChar_finLalgType := [finLalgType 'F_p of R].
+Canonical primeChar_finAlgType := [finAlgType 'F_p of R].
+ +
+Let pr_p : prime p.
+ +
+Lemma primeChar_abelem : p.-abelem [set: R].
+ +
+Lemma primeChar_pgroup : p.-group [set: R].
+ +
+Lemma order_primeChar x : x != 0 :> R → #[x]%g = p.
+ +
+Let n := logn p #|R|.
+ +
+Lemma card_primeChar : #|R| = (p ^ n)%N.
+ +
+Lemma primeChar_vectAxiom : Vector.axiom n (primeChar_lmodType charRp).
+ +
+Definition primeChar_vectMixin := Vector.Mixin primeChar_vectAxiom.
+Canonical primeChar_vectType := VectType 'F_p R primeChar_vectMixin.
+ +
+Lemma primeChar_dimf : \dim {:primeChar_vectType} = n.
+ +
+End FinRing.
+ +
+Canonical primeChar_finUnitRingType (R : finUnitRingType) charRp :=
+ [finUnitRingType of type R charRp].
+Canonical primeChar_finUnitAlgType (R : finUnitRingType) charRp :=
+ [finUnitAlgType 'F_p of type R charRp].
+Canonical primeChar_FalgType (R : finUnitRingType) charRp :=
+ [FalgType 'F_p of type R charRp].
+Canonical primeChar_finComRingType (R : finComRingType) charRp :=
+ [finComRingType of type R charRp].
+Canonical primeChar_finComUnitRingType (R : finComUnitRingType) charRp :=
+ [finComUnitRingType of type R charRp].
+Canonical primeChar_finIdomainType (R : finIdomainType) charRp :=
+ [finIdomainType of type R charRp].
+ +
+Section FinField.
+ +
+Variables (F0 : finFieldType) (charFp : p \in [char F0]).
+ +
+Canonical primeChar_finFieldType := [finFieldType of F].
+
+ We need to use the eta-long version of the constructor here as projections
+ of the Canonical fieldType of F cannot be computed syntactically.
+
+
+Canonical primeChar_fieldExtType := [fieldExtType 'F_p of F for F0].
+Canonical primeChar_splittingFieldType := FinSplittingFieldType 'F_p F.
+ +
+End FinField.
+ +
+End PrimeChar.
+ +
+Section FinSplittingField.
+ +
+Variable F : finFieldType.
+ +
+
+
++Canonical primeChar_splittingFieldType := FinSplittingFieldType 'F_p F.
+ +
+End FinField.
+ +
+End PrimeChar.
+ +
+Section FinSplittingField.
+ +
+Variable F : finFieldType.
+ +
+
+ By card_vspace order K = #|K| for any finType structure on L; however we
+ do not want to impose the FinVector instance here.
+
+
+Let order (L : vectType F) (K : {vspace L}) := (#|F| ^ \dim K)%N.
+ +
+Section FinGalois.
+ +
+Variable L : splittingFieldType F.
+Implicit Types (a b : F) (x y : L) (K E : {subfield L}).
+ +
+Let galL K : galois K {:L}.
+ +
+Fact galLgen K :
+ {alpha | generator 'Gal({:L} / K) alpha & ∀ x, alpha x = x ^+ order K}.
+ +
+Lemma finField_galois K E : (K ≤ E)%VS → galois K E.
+ +
+Lemma finField_galois_generator K E :
+ (K ≤ E)%VS →
+ {alpha | generator 'Gal(E / K) alpha
+ & {in E, ∀ x, alpha x = x ^+ order K}}.
+ +
+End FinGalois.
+ +
+Lemma Fermat's_little_theorem (L : fieldExtType F) (K : {subfield L}) a :
+ (a \in K) = (a ^+ order K == a).
+ +
+End FinSplittingField.
+ +
+Section FinFieldExists.
+
+
++ +
+Section FinGalois.
+ +
+Variable L : splittingFieldType F.
+Implicit Types (a b : F) (x y : L) (K E : {subfield L}).
+ +
+Let galL K : galois K {:L}.
+ +
+Fact galLgen K :
+ {alpha | generator 'Gal({:L} / K) alpha & ∀ x, alpha x = x ^+ order K}.
+ +
+Lemma finField_galois K E : (K ≤ E)%VS → galois K E.
+ +
+Lemma finField_galois_generator K E :
+ (K ≤ E)%VS →
+ {alpha | generator 'Gal(E / K) alpha
+ & {in E, ∀ x, alpha x = x ^+ order K}}.
+ +
+End FinGalois.
+ +
+Lemma Fermat's_little_theorem (L : fieldExtType F) (K : {subfield L}) a :
+ (a \in K) = (a ^+ order K == a).
+ +
+End FinSplittingField.
+ +
+Section FinFieldExists.
+
+ While he existence of finite splitting fields and of finite fields of
+ arbitrary prime power order is mathematically straightforward, it is
+ technically challenging to formalize in Coq. The Coq typechecker performs
+ poorly for the spme of the deeply nested dependent types used in the
+ construction, such as polynomials over extensions of extensions of finite
+ fields. Any conversion in a nested structure parameter incurs a huge
+ overhead as it is shared across term comparison by call-by-need evalution.
+ The proof of FinSplittingFieldFor is contrived to mitigate this effect:
+ the abbreviation map_poly_extField alone divides by 3 the proof checking
+ time, by reducing the number of occurrences of field(Ext)Type structures
+ in the subgoals; the succesive, apparently redundant 'suffices' localize
+ some of the conversions to smaller subgoals, yielding a further 8-fold
+ time gain. In particular, we construct the splitting field as a subtype
+ of a recursive construction rather than prove that the latter yields
+ precisely a splitting field.
+
+
+ The apparently redundant type annotation reduces checking time by 30%.
+
+
+Let map_poly_extField (F : fieldType) (L : fieldExtType F) :=
+ map_poly (in_alg L) : {poly F} → {poly L}.
+ +
+Lemma FinSplittingFieldFor (F : finFieldType) (p : {poly F}) :
+ p != 0 → {L : splittingFieldType F | splittingFieldFor 1 p^%:A {:L}}.
+ +
+Lemma PrimePowerField p k (m := (p ^ k)%N) :
+ prime p → 0 < k → {Fm : finFieldType | p \in [char Fm] & #|Fm| = m}.
+ +
+End FinFieldExists.
+ +
+Section FinDomain.
+ +
+Import ssrnum ssrint algC cyclotomic Num.Theory.
+(* Hide polynomial divisibility. *)
+ +
+Variable R : finUnitRingType.
+ +
+Hypothesis domR : GRing.IntegralDomain.axiom R.
+Implicit Types x y : R.
+ +
+Let lregR x : x != 0 → GRing.lreg x.
+ +
+Lemma finDomain_field : GRing.Field.mixin_of R.
+ +
+
+
++ map_poly (in_alg L) : {poly F} → {poly L}.
+ +
+Lemma FinSplittingFieldFor (F : finFieldType) (p : {poly F}) :
+ p != 0 → {L : splittingFieldType F | splittingFieldFor 1 p^%:A {:L}}.
+ +
+Lemma PrimePowerField p k (m := (p ^ k)%N) :
+ prime p → 0 < k → {Fm : finFieldType | p \in [char Fm] & #|Fm| = m}.
+ +
+End FinFieldExists.
+ +
+Section FinDomain.
+ +
+Import ssrnum ssrint algC cyclotomic Num.Theory.
+(* Hide polynomial divisibility. *)
+ +
+Variable R : finUnitRingType.
+ +
+Hypothesis domR : GRing.IntegralDomain.axiom R.
+Implicit Types x y : R.
+ +
+Let lregR x : x != 0 → GRing.lreg x.
+ +
+Lemma finDomain_field : GRing.Field.mixin_of R.
+ +
+
+ This is Witt's proof of Wedderburn's little theorem.
+
+
+Theorem finDomain_mulrC : @commutative R R *%R.
+ +
+Definition FinDomainFieldType : finFieldType :=
+ let fin_unit_class := FinRing.UnitRing.class R in
+ let com_class := GRing.ComRing.Class finDomain_mulrC in
+ let com_unit_class := @GRing.ComUnitRing.Class R com_class fin_unit_class in
+ let dom_class := @GRing.IntegralDomain.Class R com_unit_class domR in
+ let field_class := @GRing.Field.Class R dom_class finDomain_field in
+ let finfield_class := @FinRing.Field.Class R field_class fin_unit_class in
+ FinRing.Field.Pack finfield_class R.
+ +
+Definition FinDomainSplittingFieldType p (charRp : p \in [char R]) :=
+ let RoverFp := @primeChar_splittingFieldType p FinDomainFieldType charRp in
+ [splittingFieldType 'F_p of R for RoverFp].
+ +
+End FinDomain.
+
++ +
+Definition FinDomainFieldType : finFieldType :=
+ let fin_unit_class := FinRing.UnitRing.class R in
+ let com_class := GRing.ComRing.Class finDomain_mulrC in
+ let com_unit_class := @GRing.ComUnitRing.Class R com_class fin_unit_class in
+ let dom_class := @GRing.IntegralDomain.Class R com_unit_class domR in
+ let field_class := @GRing.Field.Class R dom_class finDomain_field in
+ let finfield_class := @FinRing.Field.Class R field_class fin_unit_class in
+ FinRing.Field.Pack finfield_class R.
+ +
+Definition FinDomainSplittingFieldType p (charRp : p \in [char R]) :=
+ let RoverFp := @primeChar_splittingFieldType p FinDomainFieldType charRp in
+ [splittingFieldType 'F_p of R for RoverFp].
+ +
+End FinDomain.
+