From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.field.fieldext.html | 646 +++++++++++++++--------------- 1 file changed, 322 insertions(+), 324 deletions(-) (limited to 'docs/htmldoc/mathcomp.field.fieldext.html') diff --git a/docs/htmldoc/mathcomp.field.fieldext.html b/docs/htmldoc/mathcomp.field.fieldext.html index 878916d..53ff8c2 100644 --- a/docs/htmldoc/mathcomp.field.fieldext.html +++ b/docs/htmldoc/mathcomp.field.fieldext.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -127,9 +126,9 @@
Record class_of T := Class {
  base : Falgebra.class_of R T;
-  comm_ext : commutative (Ring.mul base);
-  idomain_ext : IntegralDomain.axiom (Ring.Pack base T);
-  field_ext : Field.mixin_of (UnitRing.Pack base T)
+  comm_ext : commutative (Ring.mul base);
+  idomain_ext : IntegralDomain.axiom (Ring.Pack base);
+  field_ext : Field.mixin_of (UnitRing.Pack base)
}.

@@ -144,82 +143,82 @@ End Bases.

-Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
+Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.

-Variables (phR : phant R) (T : Type) (cT : type phR).
-Definition class := let: Pack _ c _ := cT return class_of cT in c.
-Let xT := let: Pack T _ _ := cT in T.
-Notation xclass := (class : class_of xT).
+Variables (phR : phant R) (T : Type) (cT : type phR).
+Definition class := let: Pack _ c := cT return class_of cT in c.
+Let xT := let: Pack T _ := cT in T.
+Notation xclass := (class : class_of xT).

Definition pack :=
  fun (bT : Falgebra.type phR) b
-    & phant_id (Falgebra.class bT : Falgebra.class_of R bT)
-               (b : Falgebra.class_of R T) ⇒
-  fun mT Cm IDm Fm & phant_id (Field.class mT) (@Field.Class T
+    & phant_id (Falgebra.class bT : Falgebra.class_of R bT)
+               (b : Falgebra.class_of R T) ⇒
+  fun mT Cm IDm Fm & phant_id (Field.class mT) (@Field.Class T
        (@IntegralDomain.Class T (@ComUnitRing.Class T (@ComRing.Class T b
-          Cm) b) IDm) Fm) ⇒ Pack phR (@Class T b Cm IDm Fm) T.
+          Cm) b) IDm) Fm) ⇒ Pack phR (@Class T b Cm IDm Fm).

Definition pack_eta K :=
  let cK := Field.class K in let Cm := ComRing.mixin cK in
  let IDm := IntegralDomain.mixin cK in let Fm := Field.mixin cK in
-  fun (bT : Falgebra.type phR) b & phant_id (Falgebra.class bT) b ⇒
-  fun cT_ & phant_id (@Class T b) cT_ ⇒ @Pack phR T (cT_ Cm IDm Fm) T.
+  fun (bT : Falgebra.type phR) b & phant_id (Falgebra.class bT) b ⇒
+  fun cT_ & phant_id (@Class T b) cT_ ⇒ @Pack phR T (cT_ Cm IDm Fm).

-Definition eqType := @Equality.Pack cT xclass xT.
-Definition choiceType := @Choice.Pack cT xclass xT.
-Definition zmodType := @Zmodule.Pack cT xclass xT.
-Definition ringType := @Ring.Pack cT xclass xT.
-Definition unitRingType := @UnitRing.Pack cT xclass xT.
-Definition comRingType := @ComRing.Pack cT xclass xT.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
-Definition idomainType := @IntegralDomain.Pack cT xclass xT.
-Definition fieldType := @Field.Pack cT xclass xT.
-Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
-Definition lalgType := @Lalgebra.Pack R phR cT xclass xT.
-Definition algType := @Algebra.Pack R phR cT xclass xT.
-Definition unitAlgType := @UnitAlgebra.Pack R phR cT xclass xT.
-Definition vectType := @Vector.Pack R phR cT xclass xT.
-Definition FalgType := @Falgebra.Pack R phR cT xclass xT.
+Definition eqType := @Equality.Pack cT xclass.
+Definition choiceType := @Choice.Pack cT xclass.
+Definition zmodType := @Zmodule.Pack cT xclass.
+Definition ringType := @Ring.Pack cT xclass.
+Definition unitRingType := @UnitRing.Pack cT xclass.
+Definition comRingType := @ComRing.Pack cT xclass.
+Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
+Definition idomainType := @IntegralDomain.Pack cT xclass.
+Definition fieldType := @Field.Pack cT xclass.
+Definition lmodType := @Lmodule.Pack R phR cT xclass.
+Definition lalgType := @Lalgebra.Pack R phR cT xclass.
+Definition algType := @Algebra.Pack R phR cT xclass.
+Definition unitAlgType := @UnitAlgebra.Pack R phR cT xclass.
+Definition vectType := @Vector.Pack R phR cT xclass.
+Definition FalgType := @Falgebra.Pack R phR cT xclass.

-Definition Falg_comRingType := @ComRing.Pack FalgType xclass xT.
-Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType xclass xT.
-Definition Falg_idomainType := @IntegralDomain.Pack FalgType xclass xT.
-Definition Falg_fieldType := @Field.Pack FalgType xclass xT.
+Definition Falg_comRingType := @ComRing.Pack FalgType xclass.
+Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType xclass.
+Definition Falg_idomainType := @IntegralDomain.Pack FalgType xclass.
+Definition Falg_fieldType := @Field.Pack FalgType xclass.

-Definition vect_comRingType := @ComRing.Pack vectType xclass xT.
-Definition vect_comUnitRingType := @ComUnitRing.Pack vectType xclass xT.
-Definition vect_idomainType := @IntegralDomain.Pack vectType xclass xT.
-Definition vect_fieldType := @Field.Pack vectType xclass xT.
+Definition vect_comRingType := @ComRing.Pack vectType xclass.
+Definition vect_comUnitRingType := @ComUnitRing.Pack vectType xclass.
+Definition vect_idomainType := @IntegralDomain.Pack vectType xclass.
+Definition vect_fieldType := @Field.Pack vectType xclass.

-Definition unitAlg_comRingType := @ComRing.Pack unitAlgType xclass xT.
-Definition unitAlg_comUnitRingType := @ComUnitRing.Pack unitAlgType xclass xT.
-Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass xT.
-Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass xT.
+Definition unitAlg_comRingType := @ComRing.Pack unitAlgType xclass.
+Definition unitAlg_comUnitRingType := @ComUnitRing.Pack unitAlgType xclass.
+Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass.
+Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass.

-Definition alg_comRingType := @ComRing.Pack algType xclass xT.
-Definition alg_comUnitRingType := @ComUnitRing.Pack algType xclass xT.
-Definition alg_idomainType := @IntegralDomain.Pack algType xclass xT.
-Definition alg_fieldType := @Field.Pack algType xclass xT.
+Definition alg_comRingType := @ComRing.Pack algType xclass.
+Definition alg_comUnitRingType := @ComUnitRing.Pack algType xclass.
+Definition alg_idomainType := @IntegralDomain.Pack algType xclass.
+Definition alg_fieldType := @Field.Pack algType xclass.

-Definition lalg_comRingType := @ComRing.Pack lalgType xclass xT.
-Definition lalg_comUnitRingType := @ComUnitRing.Pack lalgType xclass xT.
-Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass xT.
-Definition lalg_fieldType := @Field.Pack lalgType xclass xT.
+Definition lalg_comRingType := @ComRing.Pack lalgType xclass.
+Definition lalg_comUnitRingType := @ComUnitRing.Pack lalgType xclass.
+Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass.
+Definition lalg_fieldType := @Field.Pack lalgType xclass.

-Definition lmod_comRingType := @ComRing.Pack lmodType xclass xT.
-Definition lmod_comUnitRingType := @ComUnitRing.Pack lmodType xclass xT.
-Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass xT.
-Definition lmod_fieldType := @Field.Pack lmodType xclass xT.
+Definition lmod_comRingType := @ComRing.Pack lmodType xclass.
+Definition lmod_comUnitRingType := @ComUnitRing.Pack lmodType xclass.
+Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass.
+Definition lmod_fieldType := @Field.Pack lmodType xclass.

End FieldExt.
@@ -287,20 +286,20 @@ Canonical lmod_comUnitRingType.
Canonical lmod_idomainType.
Canonical lmod_fieldType.
-Notation fieldExtType R := (type (Phant R)).
+Notation fieldExtType R := (type (Phant R)).

-Notation "[ 'fieldExtType' F 'of' L ]" :=
-  (@pack _ (Phant F) L _ _ id _ _ _ _ id)
+Notation "[ 'fieldExtType' F 'of' L ]" :=
+  (@pack _ (Phant F) L _ _ id _ _ _ _ id)
  (at level 0, format "[ 'fieldExtType' F 'of' L ]") : form_scope.

-Notation "[ 'fieldExtType' F 'of' L 'for' K ]" :=
-  (@pack_eta _ (Phant F) L K _ _ id _ id)
+Notation "[ 'fieldExtType' F 'of' L 'for' K ]" :=
+  (@pack_eta _ (Phant F) L K _ _ id _ id)
  (at level 0, format "[ 'fieldExtType' F 'of' L 'for' K ]") : form_scope.

-Notation "{ 'subfield' L }" := (@aspace_of _ (FalgType _) (Phant L))
+Notation "{ 'subfield' L }" := (@aspace_of _ (FalgType _) (Phant L))
  (at level 0, format "{ 'subfield' L }") : type_scope.

@@ -309,80 +308,80 @@ Export FieldExt.Exports.

-Canonical regular_fieldExtType (F : fieldType) := [fieldExtType F of F^o for F].
+Canonical regular_fieldExtType (F : fieldType) := [fieldExtType F of F^o for F].

Section FieldExtTheory.

Variables (F0 : fieldType) (L : fieldExtType F0).
-Implicit Types (U V M : {vspace L}) (E F K : {subfield L}).
+Implicit Types (U V M : {vspace L}) (E F K : {subfield L}).

-Lemma dim_cosetv U x : x != 0 → \dim (U × <[x]>) = \dim U.
+Lemma dim_cosetv U x : x != 0 → \dim (U × <[x]>) = \dim U.

-Lemma prodvC : commutative (@prodv F0 L).
+Lemma prodvC : commutative (@prodv F0 L).
Canonical prodv_comoid := Monoid.ComLaw prodvC.

-Lemma prodvCA : left_commutative (@prodv F0 L).
+Lemma prodvCA : left_commutative (@prodv F0 L).

-Lemma prodvAC : right_commutative (@prodv F0 L).
+Lemma prodvAC : right_commutative (@prodv F0 L).

-Lemma algid1 K : algid K = 1.
+Lemma algid1 K : algid K = 1.

-Lemma mem1v K : 1 \in K.
-Lemma sub1v K : (1 ≤ K)%VS.
+Lemma mem1v K : 1 \in K.
+Lemma sub1v K : (1 ≤ K)%VS.

-Lemma subfield_closed K : agenv K = K.
+Lemma subfield_closed K : agenv K = K.

-Lemma AHom_lker0 (rT : FalgType F0) (f : 'AHom(L, rT)) : lker f == 0%VS.
+Lemma AHom_lker0 (rT : FalgType F0) (f : 'AHom(L, rT)) : lker f == 0%VS.

-Lemma AEnd_lker0 (f : 'AEnd(L)) : lker f == 0%VS.
+Lemma AEnd_lker0 (f : 'AEnd(L)) : lker f == 0%VS.

-Fact aimg_is_aspace (rT : FalgType F0) (f : 'AHom(L, rT)) (E : {subfield L}) :
-  is_aspace (f @: E).
+Fact aimg_is_aspace (rT : FalgType F0) (f : 'AHom(L, rT)) (E : {subfield L}) :
+  is_aspace (f @: E).
Canonical aimg_aspace rT f E := ASpace (@aimg_is_aspace rT f E).

-Lemma Fadjoin_idP {K x} : reflect (<<K; x>>%VS = K) (x \in K).
+Lemma Fadjoin_idP {K x} : reflect (<<K; x>>%VS = K) (x \in K).

-Lemma Fadjoin0 K : <<K; 0>>%VS = K.
+Lemma Fadjoin0 K : <<K; 0>>%VS = K.

-Lemma Fadjoin_nil K : <<K & [::]>>%VS = K.
+Lemma Fadjoin_nil K : <<K & [::]>>%VS = K.

Lemma FadjoinP {K x E} :
-  reflect (K ≤ E ∧ x \in E)%VS (<<K; x>>%AS ≤ E)%VS.
+  reflect (K ≤ E ∧ x \in E)%VS (<<K; x>>%AS ≤ E)%VS.

Lemma Fadjoin_seqP {K} {rs : seq L} {E} :
-  reflect (K ≤ E ∧ {subset rs ≤ E})%VS (<<K & rs>> ≤ E)%VS.
+  reflect (K ≤ E ∧ {subset rs ≤ E})%VS (<<K & rs>> ≤ E)%VS.

-Lemma alg_polyOver E p : map_poly (in_alg L) p \is a polyOver E.
+Lemma alg_polyOver E p : map_poly (in_alg L) p \is a polyOver E.

-Lemma sub_adjoin1v x E : (<<1; x>> ≤ E)%VS = (x \in E)%VS.
+Lemma sub_adjoin1v x E : (<<1; x>> ≤ E)%VS = (x \in E)%VS.

-Fact vsval_multiplicative K : multiplicative (vsval : subvs_of K → L).
+Fact vsval_multiplicative K : multiplicative (vsval : subvs_of K → L).
Canonical vsval_rmorphism K := AddRMorphism (vsval_multiplicative K).
-Canonical vsval_lrmorphism K : {lrmorphism subvs_of K → L} :=
-  [lrmorphism of vsval].
+Canonical vsval_lrmorphism K : {lrmorphism subvs_of K → L} :=
+  [lrmorphism of vsval].

-Lemma vsval_invf K (w : subvs_of K) : val w^-1 = (vsval w)^-1.
+Lemma vsval_invf K (w : subvs_of K) : val w^-1 = (vsval w)^-1.

Fact aspace_divr_closed K : divr_closed K.
@@ -397,110 +396,110 @@ Canonical aspace_divalgPred K := DivalgPred (memv_submod_closed K).

-Definition subvs_mulC K := [comRingMixin of subvs_of K by <:].
+Definition subvs_mulC K := [comRingMixin of subvs_of K by <:].
Canonical subvs_comRingType K :=
  Eval hnf in ComRingType (subvs_of K) (@subvs_mulC K).
Canonical subvs_comUnitRingType K :=
-  Eval hnf in [comUnitRingType of subvs_of K].
-Definition subvs_mul_eq0 K := [idomainMixin of subvs_of K by <:].
+  Eval hnf in [comUnitRingType of subvs_of K].
+Definition subvs_mul_eq0 K := [idomainMixin of subvs_of K by <:].
Canonical subvs_idomainType K :=
  Eval hnf in IdomainType (subvs_of K) (@subvs_mul_eq0 K).
Lemma subvs_fieldMixin K : GRing.Field.mixin_of (@subvs_idomainType K).
Canonical subvs_fieldType K :=
  Eval hnf in FieldType (subvs_of K) (@subvs_fieldMixin K).
-Canonical subvs_fieldExtType K := Eval hnf in [fieldExtType F0 of subvs_of K].
+Canonical subvs_fieldExtType K := Eval hnf in [fieldExtType F0 of subvs_of K].

-Lemma polyOver_subvs {K} {p : {poly L}} :
-  reflect (∃ q : {poly subvs_of K}, p = map_poly vsval q)
-          (p \is a polyOver K).
+Lemma polyOver_subvs {K} {p : {poly L}} :
+  reflect (∃ q : {poly subvs_of K}, p = map_poly vsval q)
+          (p \is a polyOver K).

-Lemma divp_polyOver K : {in polyOver K &, ∀ p q, p %/ q \is a polyOver K}.
+Lemma divp_polyOver K : {in polyOver K &, ∀ p q, p %/ q \is a polyOver K}.

-Lemma modp_polyOver K : {in polyOver K &, ∀ p q, p %% q \is a polyOver K}.
+Lemma modp_polyOver K : {in polyOver K &, ∀ p q, p %% q \is a polyOver K}.

Lemma gcdp_polyOver K :
-  {in polyOver K &, ∀ p q, gcdp p q \is a polyOver K}.
+  {in polyOver K &, ∀ p q, gcdp p q \is a polyOver K}.

-Fact prodv_is_aspace E F : is_aspace (E × F).
-Canonical prodv_aspace E F : {subfield L} := ASpace (prodv_is_aspace E F).
+Fact prodv_is_aspace E F : is_aspace (E × F).
+Canonical prodv_aspace E F : {subfield L} := ASpace (prodv_is_aspace E F).

-Fact field_mem_algid E F : algid E \in F.
-Canonical capv_aspace E F : {subfield L} := aspace_cap (field_mem_algid E F).
+Fact field_mem_algid E F : algid E \in F.
+Canonical capv_aspace E F : {subfield L} := aspace_cap (field_mem_algid E F).

-Lemma polyOverSv U V : (U ≤ V)%VS → {subset polyOver U ≤ polyOver V}.
+Lemma polyOverSv U V : (U ≤ V)%VS → {subset polyOver U ≤ polyOver V}.

-Lemma field_subvMl F U : (U ≤ F × U)%VS.
+Lemma field_subvMl F U : (U ≤ F × U)%VS.

-Lemma field_subvMr U F : (U ≤ U × F)%VS.
+Lemma field_subvMr U F : (U ≤ U × F)%VS.

-Lemma field_module_eq F M : (F × M ≤ M)%VS → (F × M)%VS = M.
+Lemma field_module_eq F M : (F × M ≤ M)%VS → (F × M)%VS = M.

-Lemma sup_field_module F E : (F × E ≤ E)%VS = (F ≤ E)%VS.
+Lemma sup_field_module F E : (F × E ≤ E)%VS = (F ≤ E)%VS.

-Lemma field_module_dimS F M : (F × M ≤ M)%VS → (\dim F %| \dim M)%N.
+Lemma field_module_dimS F M : (F × M ≤ M)%VS → (\dim F %| \dim M)%N.

-Lemma field_dimS F E : (F ≤ E)%VS → (\dim F %| \dim E)%N.
+Lemma field_dimS F E : (F ≤ E)%VS → (\dim F %| \dim E)%N.

-Lemma dim_field_module F M : (F × M ≤ M)%VS → \dim M = (\dim_F M × \dim F)%N.
+Lemma dim_field_module F M : (F × M ≤ M)%VS → \dim M = (\dim_F M × \dim F)%N.

-Lemma dim_sup_field F E : (F ≤ E)%VS → \dim E = (\dim_F E × \dim F)%N.
+Lemma dim_sup_field F E : (F ≤ E)%VS → \dim E = (\dim_F E × \dim F)%N.

-Lemma field_module_semisimple F M (m := \dim_F M) :
-    (F × M ≤ M)%VS →
-  {X : m.-tuple L | {subset X ≤ M} ∧ 0 \notin X
-     & let FX := (\sum_(i < m) F × <[X`_i]>)%VS in FX = M ∧ directv FX}.
+Lemma field_module_semisimple F M (m := \dim_F M) :
+    (F × M ≤ M)%VS →
+  {X : m.-tuple L | {subset X ≤ M} ∧ 0 \notin X
+     & let FX := (\sum_(i < m) F × <[X`_i]>)%VS in FX = M ∧ directv FX}.

Section FadjoinPolyDefinitions.

-Variables (U : {vspace L}) (x : L).
+Variables (U : {vspace L}) (x : L).

-Definition adjoin_degree := (\dim_U <<U; x>>).-1.+1.
+Definition adjoin_degree := (\dim_U <<U; x>>).-1.+1.

-Definition Fadjoin_sum := (\sum_(i < n) U × <[x ^+ i]>)%VS.
+Definition Fadjoin_sum := (\sum_(i < n) U × <[x ^+ i]>)%VS.

-Definition Fadjoin_poly v : {poly L} :=
-  \poly_(i < n) (sumv_pi Fadjoin_sum (inord i) v / x ^+ i).
+Definition Fadjoin_poly v : {poly L} :=
+  \poly_(i < n) (sumv_pi Fadjoin_sum (inord i) v / x ^+ i).

-Definition minPoly : {poly L} := 'X^n - Fadjoin_poly (x ^+ n).
+Definition minPoly : {poly L} := 'X^n - Fadjoin_poly (x ^+ n).

-Lemma size_Fadjoin_poly v : size (Fadjoin_poly v) ≤ n.
+Lemma size_Fadjoin_poly v : size (Fadjoin_poly v) ≤ n.

-Lemma Fadjoin_polyOver v : Fadjoin_poly v \is a polyOver U.
+Lemma Fadjoin_polyOver v : Fadjoin_poly v \is a polyOver U.

-Fact Fadjoin_poly_is_linear : linear_for (in_alg L \; *:%R) Fadjoin_poly.
+Fact Fadjoin_poly_is_linear : linear_for (in_alg L \; *:%R) Fadjoin_poly.
Canonical Fadjoin_poly_additive := Additive Fadjoin_poly_is_linear.
Canonical Fadjoin_poly_linear := AddLinear Fadjoin_poly_is_linear.

-Lemma size_minPoly : size minPoly = n.+1.
+Lemma size_minPoly : size minPoly = n.+1.

-Lemma monic_minPoly : minPoly \is monic.
+Lemma monic_minPoly : minPoly \is monic.

End FadjoinPolyDefinitions.
@@ -509,85 +508,85 @@ Section FadjoinPoly.

-Variables (K : {subfield L}) (x : L).
+Variables (K : {subfield L}) (x : L).

-Lemma adjoin_degreeE : n = \dim_K <<K; x>>.
+Lemma adjoin_degreeE : n = \dim_K <<K; x>>.

-Lemma dim_Fadjoin : \dim <<K; x>> = (n × \dim K)%N.
+Lemma dim_Fadjoin : \dim <<K; x>> = (n × \dim K)%N.

-Lemma adjoin0_deg : adjoin_degree K 0 = 1%N.
+Lemma adjoin0_deg : adjoin_degree K 0 = 1%N.

-Lemma adjoin_deg_eq1 : (n == 1%N) = (x \in K).
+Lemma adjoin_deg_eq1 : (n == 1%N) = (x \in K).

Lemma Fadjoin_sum_direct : directv sumKx.

-Let nz_x_i (i : 'I_n) : x ^+ i != 0.
+Let nz_x_i (i : 'I_n) : x ^+ i != 0.

-Lemma Fadjoin_eq_sum : <<K; x>>%VS = sumKx.
+Lemma Fadjoin_eq_sum : <<K; x>>%VS = sumKx.

-Lemma Fadjoin_poly_eq v : v \in <<K; x>>%VS → (Fadjoin_poly K x v).[x] = v.
+Lemma Fadjoin_poly_eq v : v \in <<K; x>>%VS → (Fadjoin_poly K x v).[x] = v.

-Lemma mempx_Fadjoin p : p \is a polyOver K → p.[x] \in <<K; x>>%VS.
+Lemma mempx_Fadjoin p : p \is a polyOver K → p.[x] \in <<K; x>>%VS.

Lemma Fadjoin_polyP {v} :
-  reflect (exists2 p, p \in polyOver K & v = p.[x]) (v \in <<K; x>>%VS).
+  reflect (exists2 p, p \in polyOver K & v = p.[x]) (v \in <<K; x>>%VS).

Lemma Fadjoin_poly_unique p v :
-  p \is a polyOver K → size p ≤ n → p.[x] = v → Fadjoin_poly K x v = p.
+  p \is a polyOver K → size p ≤ n → p.[x] = v → Fadjoin_poly K x v = p.

-Lemma Fadjoin_polyC v : v \in K → Fadjoin_poly K x v = v%:P.
+Lemma Fadjoin_polyC v : v \in K → Fadjoin_poly K x v = v%:P.

-Lemma Fadjoin_polyX : x \notin K → Fadjoin_poly K x x = 'X.
+Lemma Fadjoin_polyX : x \notin K → Fadjoin_poly K x x = 'X.

-Lemma minPolyOver : minPoly K x \is a polyOver K.
+Lemma minPolyOver : minPoly K x \is a polyOver K.

-Lemma minPolyxx : (minPoly K x).[x] = 0.
+Lemma minPolyxx : (minPoly K x).[x] = 0.

Lemma root_minPoly : root (minPoly K x) x.

Lemma Fadjoin_poly_mod p :
-  p \is a polyOver K → Fadjoin_poly K x p.[x] = p %% minPoly K x.
+  p \is a polyOver K → Fadjoin_poly K x p.[x] = p %% minPoly K x.

-Lemma minPoly_XsubC : reflect (minPoly K x = 'X - x%:P) (x \in K).
+Lemma minPoly_XsubC : reflect (minPoly K x = 'X - x%:P) (x \in K).

Lemma root_small_adjoin_poly p :
-  p \is a polyOver K → size p ≤ n → root p x = (p == 0).
+  p \is a polyOver K → size p ≤ n → root p x = (p == 0).

Lemma minPoly_irr p :
-  p \is a polyOver K → p %| minPoly K x → (p %= minPoly K x) || (p %= 1).
+  p \is a polyOver K → p %| minPoly K x → (p %= minPoly K x) || (p %= 1).

-Lemma minPoly_dvdp p : p \is a polyOver K → root p x → (minPoly K x) %| p.
+Lemma minPoly_dvdp p : p \is a polyOver K → root p x → (minPoly K x) %| p.

End FadjoinPoly.

-Lemma minPolyS K E a : (K ≤ E)%VS → minPoly E a %| minPoly K a.
+Lemma minPolyS K E a : (K ≤ E)%VS → minPoly E a %| minPoly K a.

Lemma Fadjoin1_polyP x v :
-  reflect (∃ p, v = (map_poly (in_alg L) p).[x]) (v \in <<1; x>>%VS).
+  reflect (∃ p, v = (map_poly (in_alg L) p).[x]) (v \in <<1; x>>%VS).

Section Horner.
@@ -597,13 +596,13 @@
Definition fieldExt_horner := horner_morph (fun x ⇒ mulrC z (in_alg L x)).
-Canonical fieldExtHorner_additive := [additive of fieldExt_horner].
-Canonical fieldExtHorner_rmorphism := [rmorphism of fieldExt_horner].
-Lemma fieldExt_hornerC b : fieldExt_horner b%:P = b%:A.
- Lemma fieldExt_hornerX : fieldExt_horner 'X = z.
+Canonical fieldExtHorner_additive := [additive of fieldExt_horner].
+Canonical fieldExtHorner_rmorphism := [rmorphism of fieldExt_horner].
+Lemma fieldExt_hornerC b : fieldExt_horner b%:P = b%:A.
+ Lemma fieldExt_hornerX : fieldExt_horner 'X = z.
Fact fieldExt_hornerZ : scalable fieldExt_horner.
Canonical fieldExt_horner_linear := AddLinear fieldExt_hornerZ.
-Canonical fieldExt_horner_lrmorhism := [lrmorphism of fieldExt_horner].
+Canonical fieldExt_horner_lrmorhism := [lrmorphism of fieldExt_horner].

End Horner.
@@ -612,15 +611,15 @@ End FieldExtTheory.

-Notation "E :&: F" := (capv_aspace E F) : aspace_scope.
-Notation "'C_ E [ x ]" := (capv_aspace E 'C[x]) : aspace_scope.
-Notation "'C_ ( E ) [ x ]" := (capv_aspace E 'C[x])
+Notation "E :&: F" := (capv_aspace E F) : aspace_scope.
+Notation "'C_ E [ x ]" := (capv_aspace E 'C[x]) : aspace_scope.
+Notation "'C_ ( E ) [ x ]" := (capv_aspace E 'C[x])
  (only parsing) : aspace_scope.
-Notation "'C_ E ( V )" := (capv_aspace E 'C(V)) : aspace_scope.
-Notation "'C_ ( E ) ( V )" := (capv_aspace E 'C(V))
+Notation "'C_ E ( V )" := (capv_aspace E 'C(V)) : aspace_scope.
+Notation "'C_ ( E ) ( V )" := (capv_aspace E 'C(V))
  (only parsing) : aspace_scope.
-Notation "E * F" := (prodv_aspace E F) : aspace_scope.
-Notation "f @: E" := (aimg_aspace f E) : aspace_scope.
+Notation "E * F" := (prodv_aspace E F) : aspace_scope.
+Notation "f @: E" := (aimg_aspace f E) : aspace_scope.

@@ -628,14 +627,14 @@ Section MapMinPoly.

-Variables (F0 : fieldType) (L rL : fieldExtType F0) (f : 'AHom(L, rL)).
-Variables (K : {subfield L}) (x : L).
+Variables (F0 : fieldType) (L rL : fieldExtType F0) (f : 'AHom(L, rL)).
+Variables (K : {subfield L}) (x : L).

-Lemma adjoin_degree_aimg : adjoin_degree (f @: K) (f x) = adjoin_degree K x.
+Lemma adjoin_degree_aimg : adjoin_degree (f @: K) (f x) = adjoin_degree K x.

-Lemma map_minPoly : map_poly f (minPoly K x) = minPoly (f @: K) (f x).
+Lemma map_minPoly : map_poly f (minPoly K x) = minPoly (f @: K) (f x).

End MapMinPoly.
@@ -650,36 +649,36 @@ Section FieldOver.

-Variables (F0 : fieldType) (L : fieldExtType F0) (F : {subfield L}).
+Variables (F0 : fieldType) (L : fieldExtType F0) (F : {subfield L}).

-Definition fieldOver of {vspace L} : Type := L.
+Definition fieldOver of {vspace L} : Type := L.

-Canonical fieldOver_eqType := [eqType of L_F].
-Canonical fieldOver_choiceType := [choiceType of L_F].
-Canonical fieldOver_zmodType := [zmodType of L_F].
-Canonical fieldOver_ringType := [ringType of L_F].
-Canonical fieldOver_unitRingType := [unitRingType of L_F].
-Canonical fieldOver_comRingType := [comRingType of L_F].
-Canonical fieldOver_comUnitRingType := [comUnitRingType of L_F].
-Canonical fieldOver_idomainType := [idomainType of L_F].
-Canonical fieldOver_fieldType := [fieldType of L_F].
+Canonical fieldOver_eqType := [eqType of L_F].
+Canonical fieldOver_choiceType := [choiceType of L_F].
+Canonical fieldOver_zmodType := [zmodType of L_F].
+Canonical fieldOver_ringType := [ringType of L_F].
+Canonical fieldOver_unitRingType := [unitRingType of L_F].
+Canonical fieldOver_comRingType := [comRingType of L_F].
+Canonical fieldOver_comUnitRingType := [comUnitRingType of L_F].
+Canonical fieldOver_idomainType := [idomainType of L_F].
+Canonical fieldOver_fieldType := [fieldType of L_F].

-Definition fieldOver_scale (a : K_F) (u : L_F) : L_F := vsval a × u.
+Definition fieldOver_scale (a : K_F) (u : L_F) : L_F := vsval a × u.

-Fact fieldOver_scaleA a b u : a ×F: (b ×F: u) = (a × b) ×F: u.
+Fact fieldOver_scaleA a b u : a ×F: (b ×F: u) = (a × b) ×F: u.

-Fact fieldOver_scale1 u : 1 ×F: u = u.
+Fact fieldOver_scale1 u : 1 ×F: u = u.

-Fact fieldOver_scaleDr a u v : a ×F: (u + v) = a ×F: u + a ×F: v.
+Fact fieldOver_scaleDr a u v : a ×F: (u + v) = a ×F: u + a ×F: v.

-Fact fieldOver_scaleDl v a b : (a + b) ×F: v = a ×F: v + b ×F: v.
+Fact fieldOver_scaleDl v a b : (a + b) ×F: v = a ×F: v + b ×F: v.

Definition fieldOver_lmodMixin :=
@@ -690,61 +689,61 @@ Canonical fieldOver_lmodType := LmodType K_F L_F fieldOver_lmodMixin.

-Lemma fieldOver_scaleE a (u : L) : a *: (u : L_F) = vsval a × u.
+Lemma fieldOver_scaleE a (u : L) : a *: (u : L_F) = vsval a × u.

-Fact fieldOver_scaleAl a u v : a ×F: (u × v) = (a ×F: u) × v.
+Fact fieldOver_scaleAl a u v : a ×F: (u × v) = (a ×F: u) × v.

Canonical fieldOver_lalgType := LalgType K_F L_F fieldOver_scaleAl.

-Fact fieldOver_scaleAr a u v : a ×F: (u × v) = u × (a ×F: v).
+Fact fieldOver_scaleAr a u v : a ×F: (u × v) = u × (a ×F: v).

Canonical fieldOver_algType := AlgType K_F L_F fieldOver_scaleAr.
-Canonical fieldOver_unitAlgType := [unitAlgType K_F of L_F].
+Canonical fieldOver_unitAlgType := [unitAlgType K_F of L_F].

Fact fieldOver_vectMixin : Vector.mixin_of fieldOver_lmodType.

Canonical fieldOver_vectType := VectType K_F L_F fieldOver_vectMixin.
-Canonical fieldOver_FalgType := [FalgType K_F of L_F].
-Canonical fieldOver_fieldExtType := [fieldExtType K_F of L_F].
+Canonical fieldOver_FalgType := [FalgType K_F of L_F].
+Canonical fieldOver_fieldExtType := [fieldExtType K_F of L_F].

-Implicit Types (V : {vspace L}) (E : {subfield L}).
+Implicit Types (V : {vspace L}) (E : {subfield L}).

-Lemma trivial_fieldOver : (1%VS : {vspace L_F}) =i F.
+Lemma trivial_fieldOver : (1%VS : {vspace L_F}) =i F.

-Definition vspaceOver V := <<vbasis V : seq L_F>>%VS.
+Definition vspaceOver V := <<vbasis V : seq L_F>>%VS.

-Lemma mem_vspaceOver V : vspaceOver V =i (F × V)%VS.
+Lemma mem_vspaceOver V : vspaceOver V =i (F × V)%VS.

-Lemma mem_aspaceOver E : (F ≤ E)%VS → vspaceOver E =i E.
+Lemma mem_aspaceOver E : (F ≤ E)%VS → vspaceOver E =i E.

Fact aspaceOver_suproof E : is_aspace (vspaceOver E).
Canonical aspaceOver E := ASpace (aspaceOver_suproof E).

-Lemma dim_vspaceOver M : (F × M ≤ M)%VS → \dim (vspaceOver M) = \dim_F M.
+Lemma dim_vspaceOver M : (F × M ≤ M)%VS → \dim (vspaceOver M) = \dim_F M.

-Lemma dim_aspaceOver E : (F ≤ E)%VS → \dim (vspaceOver E) = \dim_F E.
+Lemma dim_aspaceOver E : (F ≤ E)%VS → \dim (vspaceOver E) = \dim_F E.

Lemma vspaceOverP V_F :
-  {V | [/\ V_F = vspaceOver V, (F × V ≤ V)%VS & V_F =i V]}.
+  {V | [/\ V_F = vspaceOver V, (F × V ≤ V)%VS & V_F =i V]}.

-Lemma aspaceOverP (E_F : {subfield L_F}) :
-  {E | [/\ E_F = aspaceOver E, (F ≤ E)%VS & E_F =i E]}.
+Lemma aspaceOverP (E_F : {subfield L_F}) :
+  {E | [/\ E_F = aspaceOver E, (F ≤ E)%VS & E_F =i E]}.

End FieldOver.
@@ -762,34 +761,34 @@ Variables (F0 : fieldType) (F : fieldExtType F0) (L : fieldExtType F).

-Definition baseField_type of phant L : Type := L.
-Notation L0 := (baseField_type (Phant (FieldExt.sort L))).
+Definition baseField_type of phant L : Type := L.
+Notation L0 := (baseField_type (Phant (FieldExt.sort L))).

-Canonical baseField_eqType := [eqType of L0].
-Canonical baseField_choiceType := [choiceType of L0].
-Canonical baseField_zmodType := [zmodType of L0].
-Canonical baseField_ringType := [ringType of L0].
-Canonical baseField_unitRingType := [unitRingType of L0].
-Canonical baseField_comRingType := [comRingType of L0].
-Canonical baseField_comUnitRingType := [comUnitRingType of L0].
-Canonical baseField_idomainType := [idomainType of L0].
-Canonical baseField_fieldType := [fieldType of L0].
+Canonical baseField_eqType := [eqType of L0].
+Canonical baseField_choiceType := [choiceType of L0].
+Canonical baseField_zmodType := [zmodType of L0].
+Canonical baseField_ringType := [ringType of L0].
+Canonical baseField_unitRingType := [unitRingType of L0].
+Canonical baseField_comRingType := [comRingType of L0].
+Canonical baseField_comUnitRingType := [comUnitRingType of L0].
+Canonical baseField_idomainType := [idomainType of L0].
+Canonical baseField_fieldType := [fieldType of L0].

-Definition baseField_scale (a : F0) (u : L0) : L0 := in_alg F a *: u.
+Definition baseField_scale (a : F0) (u : L0) : L0 := in_alg F a *: u.

-Fact baseField_scaleA a b u : a ×F0: (b ×F0: u) = (a × b) ×F0: u.
+Fact baseField_scaleA a b u : a ×F0: (b ×F0: u) = (a × b) ×F0: u.

-Fact baseField_scale1 u : 1 ×F0: u = u.
+Fact baseField_scale1 u : 1 ×F0: u = u.

-Fact baseField_scaleDr a u v : a ×F0: (u + v) = a ×F0: u + a ×F0: v.
+Fact baseField_scaleDr a u v : a ×F0: (u + v) = a ×F0: u + a ×F0: v.

-Fact baseField_scaleDl v a b : (a + b) ×F0: v = a ×F0: v + b ×F0: v.
+Fact baseField_scaleDl v a b : (a + b) ×F0: v = a ×F0: v + b ×F0: v.

Definition baseField_lmodMixin :=
@@ -800,24 +799,24 @@ Canonical baseField_lmodType := LmodType F0 L0 baseField_lmodMixin.

-Lemma baseField_scaleE a (u : L) : a *: (u : L0) = a%:A *: u.
+Lemma baseField_scaleE a (u : L) : a *: (u : L0) = a%:A *: u.

-Fact baseField_scaleAl a (u v : L0) : a ×F0: (u × v) = (a ×F0: u) × v.
+Fact baseField_scaleAl a (u v : L0) : a ×F0: (u × v) = (a ×F0: u) × v.

Canonical baseField_lalgType := LalgType F0 L0 baseField_scaleAl.

-Fact baseField_scaleAr a u v : a ×F0: (u × v) = u × (a ×F0: v).
+Fact baseField_scaleAr a u v : a ×F0: (u × v) = u × (a ×F0: v).

Canonical baseField_algType := AlgType F0 L0 baseField_scaleAr.
-Canonical baseField_unitAlgType := [unitAlgType F0 of L0].
+Canonical baseField_unitAlgType := [unitAlgType F0 of L0].

-Let n := \dim {:F}.
-Let bF : n.-tuple F := vbasis {:F}.
+Let n := \dim {:F}.
+Let bF : n.-tuple F := vbasis {:F}.
Let coordF (x : F) := (coord_vbasis (memvf x)).

@@ -825,58 +824,58 @@
Canonical baseField_vectType := VectType F0 L0 baseField_vectMixin.
-Canonical baseField_FalgType := [FalgType F0 of L0].
-Canonical baseField_extFieldType := [fieldExtType F0 of L0].
+Canonical baseField_FalgType := [FalgType F0 of L0].
+Canonical baseField_extFieldType := [fieldExtType F0 of L0].

-Let F0ZEZ a x v : a *: ((x *: v : L) : L0) = (a *: x) *: v.
+Let F0ZEZ a x v : a *: ((x *: v : L) : L0) = (a *: x) *: v.

Let baseVspace_basis V : seq L0 :=
-  [seq tnth bF ij.2 *: tnth (vbasis V) ij.1 | ij : 'I_(\dim V) × 'I_n].
-Definition baseVspace V := <<baseVspace_basis V>>%VS.
+  [seq tnth bF ij.2 *: tnth (vbasis V) ij.1 | ij : 'I_(\dim V) × 'I_n].
+Definition baseVspace V := <<baseVspace_basis V>>%VS.

-Lemma mem_baseVspace V : baseVspace V =i V.
+Lemma mem_baseVspace V : baseVspace V =i V.

-Lemma dim_baseVspace V : \dim (baseVspace V) = (\dim V × n)%N.
+Lemma dim_baseVspace V : \dim (baseVspace V) = (\dim V × n)%N.

-Fact baseAspace_suproof (E : {subfield L}) : is_aspace (baseVspace E).
+Fact baseAspace_suproof (E : {subfield L}) : is_aspace (baseVspace E).
Canonical baseAspace E := ASpace (baseAspace_suproof E).

-Fact refBaseField_key : unit.
-Definition refBaseField := locked_with refBaseField_key (baseAspace 1).
-Canonical refBaseField_unlockable := [unlockable of refBaseField].
+Fact refBaseField_key : unit.
+Definition refBaseField := locked_with refBaseField_key (baseAspace 1).
+Canonical refBaseField_unlockable := [unlockable of refBaseField].
Notation F1 := refBaseField.

-Lemma dim_refBaseField : \dim F1 = n.
+Lemma dim_refBaseField : \dim F1 = n.

-Lemma baseVspace_module V (V0 := baseVspace V) : (F1 × V0 ≤ V0)%VS.
+Lemma baseVspace_module V (V0 := baseVspace V) : (F1 × V0 ≤ V0)%VS.

-Lemma sub_baseField (E : {subfield L}) : (F1 ≤ baseVspace E)%VS.
+Lemma sub_baseField (E : {subfield L}) : (F1 ≤ baseVspace E)%VS.

-Lemma vspaceOver_refBase V : vspaceOver F1 (baseVspace V) =i V.
+Lemma vspaceOver_refBase V : vspaceOver F1 (baseVspace V) =i V.

Lemma module_baseVspace M0 :
-  (F1 × M0 ≤ M0)%VS → {V | M0 = baseVspace V & M0 =i V}.
+  (F1 × M0 ≤ M0)%VS → {V | M0 = baseVspace V & M0 =i V}.

-Lemma module_baseAspace (E0 : {subfield L0}) :
-  (F1 ≤ E0)%VS → {E | E0 = baseAspace E & E0 =i E}.
+Lemma module_baseAspace (E0 : {subfield L0}) :
+  (F1 ≤ E0)%VS → {E | E0 = baseAspace E & E0 =i E}.

End BaseField.

-Notation baseFieldType L := (baseField_type (Phant L)).
+Notation baseFieldType L := (baseField_type (Phant L)).

@@ -888,17 +887,17 @@ Section MoreFieldOver.

-Variables (F0 : fieldType) (L : fieldExtType F0) (F : {subfield L}).
+Variables (F0 : fieldType) (L : fieldExtType F0) (F : {subfield L}).

-Lemma base_vspaceOver V : baseVspace (vspaceOver F V) =i (F × V)%VS.
+Lemma base_vspaceOver V : baseVspace (vspaceOver F V) =i (F × V)%VS.

-Lemma base_moduleOver V : (F × V ≤ V)%VS → baseVspace (vspaceOver F V) =i V.
+Lemma base_moduleOver V : (F × V ≤ V)%VS → baseVspace (vspaceOver F V) =i V.

-Lemma base_aspaceOver (E : {subfield L}) :
-  (F ≤ E)%VS → baseVspace (vspaceOver F E) =i E.
+Lemma base_aspaceOver (E : {subfield L}) :
+  (F ≤ E)%VS → baseVspace (vspaceOver F E) =i E.

End MoreFieldOver.
@@ -910,35 +909,35 @@ Local Open Scope quotient_scope.

-Variables (F L : fieldType) (iota : {rmorphism F → L}).
-Variables (z : L) (p : {poly F}).
+Variables (F L : fieldType) (iota : {rmorphism F → L}).
+Variables (z : L) (p : {poly F}).


-Let wf_p := (p != 0) && root p^iota z.
-Let p0 : {poly F} := if wf_p then (lead_coef p)^-1 *: p else 'X.
-Let z0 := if wf_p then z else 0.
-Let n := (size p0).-1.
+Let wf_p := (p != 0) && root p^iota z.
+Let p0 : {poly F} := if wf_p then (lead_coef p)^-1 *: p else 'X.
+Let z0 := if wf_p then z else 0.
+Let n := (size p0).-1.

-Let p0_mon : p0 \is monic.
+Let p0_mon : p0 \is monic.

-Let nz_p0 : p0 != 0.
+Let nz_p0 : p0 != 0.

-Let p0z0 : root p0^iota z0.
+Let p0z0 : root p0^iota z0.

-Let n_gt0: 0 < n.
+Let n_gt0: 0 < n.

Let z0Ciota : commr_rmorph iota z0.
-Let iotaFz (x : 'rV[F]_n) := iotaPz (rVpoly x).
+Let iotaFz (x : 'rV[F]_n) := iotaPz (rVpoly x).

-Definition equiv_subfext x y := (iotaFz x == iotaFz y).
+Definition equiv_subfext x y := (iotaFz x == iotaFz y).

Fact equiv_subfext_is_equiv : equiv_class_of equiv_subfext.
@@ -948,47 +947,47 @@ Canonical equiv_subfext_encModRel := defaultEncModRel equiv_subfext.

-Definition subFExtend := {eq_quot equiv_subfext}.
-Canonical subFExtend_eqType := [eqType of subFExtend].
-Canonical subFExtend_choiceType := [choiceType of subFExtend].
-Canonical subFExtend_quotType := [quotType of subFExtend].
-Canonical subFExtend_eqQuotType := [eqQuotType equiv_subfext of subFExtend].
+Definition subFExtend := {eq_quot equiv_subfext}.
+Canonical subFExtend_eqType := [eqType of subFExtend].
+Canonical subFExtend_choiceType := [choiceType of subFExtend].
+Canonical subFExtend_quotType := [quotType of subFExtend].
+Canonical subFExtend_eqQuotType := [eqQuotType equiv_subfext of subFExtend].

Definition subfx_inj := lift_fun1 subFExtend iotaFz.

-Fact pi_subfx_inj : {mono \pi : x / iotaFz x >-> subfx_inj x}.
+Fact pi_subfx_inj : {mono \pi : x / iotaFz x >-> subfx_inj x}.
Canonical pi_subfx_inj_morph := PiMono1 pi_subfx_inj.

-Let iotaPz_repr x : iotaPz (rVpoly (repr (\pi_(subFExtend) x))) = iotaFz x.
+Let iotaPz_repr x : iotaPz (rVpoly (repr (\pi_(subFExtend) x))) = iotaFz x.

Definition subfext0 := lift_cst subFExtend 0.
Canonical subfext0_morph := PiConst subfext0.

-Definition subfext_add := lift_op2 subFExtend +%R.
-Fact pi_subfext_add : {morph \pi : x y / x + y >-> subfext_add x y}.
+Definition subfext_add := lift_op2 subFExtend +%R.
+Fact pi_subfext_add : {morph \pi : x y / x + y >-> subfext_add x y}.
Canonical pi_subfx_add_morph := PiMorph2 pi_subfext_add.

-Definition subfext_opp := lift_op1 subFExtend -%R.
-Fact pi_subfext_opp : {morph \pi : x / - x >-> subfext_opp x}.
+Definition subfext_opp := lift_op1 subFExtend -%R.
+Fact pi_subfext_opp : {morph \pi : x / - x >-> subfext_opp x}.
Canonical pi_subfext_opp_morph := PiMorph1 pi_subfext_opp.

-Fact addfxA : associative subfext_add.
+Fact addfxA : associative subfext_add.

-Fact addfxC : commutative subfext_add.
+Fact addfxC : commutative subfext_add.

-Fact add0fx : left_id subfext0 subfext_add.
+Fact add0fx : left_id subfext0 subfext_add.

-Fact addfxN : left_inverse subfext0 subfext_opp subfext_add.
+Fact addfxN : left_inverse subfext0 subfext_opp subfext_add.

Definition subfext_zmodMixin := ZmodMixin addfxA addfxC add0fx addfxN.
@@ -996,19 +995,19 @@   Eval hnf in ZmodType subFExtend subfext_zmodMixin.

-Let poly_rV_modp_K q : rVpoly (poly_rV (q %% p0) : 'rV[F]_n) = q %% p0.
+Let poly_rV_modp_K q : rVpoly (poly_rV (q %% p0) : 'rV[F]_n) = q %% p0.

-Let iotaPz_modp q : iotaPz (q %% p0) = iotaPz q.
+Let iotaPz_modp q : iotaPz (q %% p0) = iotaPz q.

-Definition subfx_mul_rep (x y : 'rV[F]_n) : 'rV[F]_n :=
-  poly_rV ((rVpoly x) × (rVpoly y) %% p0).
+Definition subfx_mul_rep (x y : 'rV[F]_n) : 'rV[F]_n :=
+  poly_rV ((rVpoly x) × (rVpoly y) %% p0).

Definition subfext_mul := lift_op2 subFExtend subfx_mul_rep.
Fact pi_subfext_mul :
-  {morph \pi : x y / subfx_mul_rep x y >-> subfext_mul x y}.
+  {morph \pi : x y / subfx_mul_rep x y >-> subfext_mul x y}.
Canonical pi_subfext_mul_morph := PiMorph2 pi_subfext_mul.

@@ -1016,19 +1015,19 @@ Canonical subfext1_morph := PiConst subfext1.

-Fact mulfxA : associative (subfext_mul).
+Fact mulfxA : associative (subfext_mul).

-Fact mulfxC : commutative subfext_mul.
+Fact mulfxC : commutative subfext_mul.

-Fact mul1fx : left_id subfext1 subfext_mul.
+Fact mul1fx : left_id subfext1 subfext_mul.

-Fact mulfx_addl : left_distributive subfext_mul subfext_add.
+Fact mulfx_addl : left_distributive subfext_mul subfext_add.

-Fact nonzero1fx : subfext1 != subfext0.
+Fact nonzero1fx : subfext1 != subfext0.

Definition subfext_comRingMixin :=
@@ -1037,35 +1036,35 @@ Canonical subfext_comRing := Eval hnf in ComRingType subFExtend mulfxC.

-Definition subfx_poly_inv (q : {poly F}) : {poly F} :=
-  if iotaPz q == 0 then 0 else
-  let r := gdcop q p0 in let: (u, v) := egcdp q r in
-  ((u × q + v × r)`_0)^-1 *: u.
+Definition subfx_poly_inv (q : {poly F}) : {poly F} :=
+  if iotaPz q == 0 then 0 else
+  let r := gdcop q p0 in let: (u, v) := egcdp q r in
+  ((u × q + v × r)`_0)^-1 *: u.

-Let subfx_poly_invE q : iotaPz (subfx_poly_inv q) = (iotaPz q)^-1.
+Let subfx_poly_invE q : iotaPz (subfx_poly_inv q) = (iotaPz q)^-1.

-Definition subfx_inv_rep (x : 'rV[F]_n) : 'rV[F]_n :=
-  poly_rV (subfx_poly_inv (rVpoly x) %% p0).
+Definition subfx_inv_rep (x : 'rV[F]_n) : 'rV[F]_n :=
+  poly_rV (subfx_poly_inv (rVpoly x) %% p0).

Definition subfext_inv := lift_op1 subFExtend subfx_inv_rep.
-Fact pi_subfext_inv : {morph \pi : x / subfx_inv_rep x >-> subfext_inv x}.
+Fact pi_subfext_inv : {morph \pi : x / subfx_inv_rep x >-> subfext_inv x}.
Canonical pi_subfext_inv_morph := PiMorph1 pi_subfext_inv.

Fact subfx_fieldAxiom :
-  GRing.Field.axiom (subfext_inv : subFExtend → subFExtend).
+  GRing.Field.axiom (subfext_inv : subFExtend → subFExtend).

-Fact subfx_inv0 : subfext_inv (0 : subFExtend) = (0 : subFExtend).
+Fact subfx_inv0 : subfext_inv (0 : subFExtend) = (0 : subFExtend).

Definition subfext_unitRingMixin := FieldUnitMixin subfx_fieldAxiom subfx_inv0.
Canonical subfext_unitRingType :=
  Eval hnf in UnitRingType subFExtend subfext_unitRingMixin.
-Canonical subfext_comUnitRing := Eval hnf in [comUnitRingType of subFExtend].
+Canonical subfext_comUnitRing := Eval hnf in [comUnitRingType of subFExtend].
Definition subfext_fieldMixin := @FieldMixin _ _ subfx_fieldAxiom subfx_inv0.
Definition subfext_idomainMixin := FieldIdomainMixin subfext_fieldMixin.
Canonical subfext_idomainType :=
@@ -1079,11 +1078,11 @@ Canonical subfx_inj_rmorphism := RMorphism subfx_inj_is_rmorphism.

-Definition subfx_eval := lift_embed subFExtend (fun q ⇒ poly_rV (q %% p0)).
+Definition subfx_eval := lift_embed subFExtend (fun q ⇒ poly_rV (q %% p0)).
Canonical subfx_eval_morph := PiEmbed subfx_eval.

-Definition subfx_root := subfx_eval 'X.
+Definition subfx_root := subfx_eval 'X.

Lemma subfx_eval_is_rmorphism : rmorphism subfx_eval.
@@ -1091,65 +1090,65 @@ Canonical subfx_eval_rmorphism := AddRMorphism subfx_eval_is_rmorphism.

-Definition inj_subfx := (subfx_eval \o polyC).
-Canonical inj_subfx_addidive := [additive of inj_subfx].
-Canonical inj_subfx_rmorphism := [rmorphism of inj_subfx].
+Definition inj_subfx := (subfx_eval \o polyC).
+Canonical inj_subfx_addidive := [additive of inj_subfx].
+Canonical inj_subfx_rmorphism := [rmorphism of inj_subfx].

-Lemma subfxE x: ∃ p, x = subfx_eval p.
+Lemma subfxE x: ∃ p, x = subfx_eval p.

-Definition subfx_scale a x := inj_subfx a × x.
+Definition subfx_scale a x := inj_subfx a × x.
Fact subfx_scalerA a b x :
-  subfx_scale a (subfx_scale b x) = subfx_scale (a × b) x.
- Fact subfx_scaler1r : left_id 1 subfx_scale.
- Fact subfx_scalerDr : right_distributive subfx_scale +%R.
- Fact subfx_scalerDl x : {morph subfx_scale^~ x : a b / a + b}.
+  subfx_scale a (subfx_scale b x) = subfx_scale (a × b) x.
+ Fact subfx_scaler1r : left_id 1 subfx_scale.
+ Fact subfx_scalerDr : right_distributive subfx_scale +%R.
+ Fact subfx_scalerDl x : {morph subfx_scale^~ x : a b / a + b}.
Definition subfx_lmodMixin :=
  LmodMixin subfx_scalerA subfx_scaler1r subfx_scalerDr subfx_scalerDl.
Canonical subfx_lmodType := LmodType F subFExtend subfx_lmodMixin.

-Fact subfx_scaleAl : GRing.Lalgebra.axiom ( *%R : subFExtend → _).
+Fact subfx_scaleAl : GRing.Lalgebra.axiom ( *%R : subFExtend → _).
Canonical subfx_lalgType := LalgType F subFExtend subfx_scaleAl.

Fact subfx_scaleAr : GRing.Algebra.axiom subfx_lalgType.
Canonical subfx_algType := AlgType F subFExtend subfx_scaleAr.
-Canonical subfext_unitAlgType := [unitAlgType F of subFExtend].
+Canonical subfext_unitAlgType := [unitAlgType F of subFExtend].

Fact subfx_evalZ : scalable subfx_eval.
Canonical subfx_eval_linear := AddLinear subfx_evalZ.
-Canonical subfx_eval_lrmorphism := [lrmorphism of subfx_eval].
+Canonical subfx_eval_lrmorphism := [lrmorphism of subfx_eval].

-Hypothesis (pz0 : root p^iota z).
+Hypothesis (pz0 : root p^iota z).

Section NonZero.

-Hypothesis nz_p : p != 0.
+Hypothesis nz_p : p != 0.

-Lemma subfx_inj_eval q : subfx_inj (subfx_eval q) = q^iota.[z].
+Lemma subfx_inj_eval q : subfx_inj (subfx_eval q) = q^iota.[z].

-Lemma subfx_inj_root : subfx_inj subfx_root = z.
+Lemma subfx_inj_root : subfx_inj subfx_root = z.

-Lemma subfx_injZ b x : subfx_inj (b *: x) = iota b × subfx_inj x.
+Lemma subfx_injZ b x : subfx_inj (b *: x) = iota b × subfx_inj x.

-Lemma subfx_inj_base b : subfx_inj b%:A = iota b.
+Lemma subfx_inj_base b : subfx_inj b%:A = iota b.

-Lemma subfxEroot x : {q | x = (map_poly (in_alg subFExtend) q).[subfx_root]}.
+Lemma subfxEroot x : {q | x = (map_poly (in_alg subFExtend) q).[subfx_root]}.

Lemma subfx_irreducibleP :
- (∀ q, root q^iota z → q != 0 → size p ≤ size q) ↔ irreducible_poly p.
+ (∀ q, root q^iota z → q != 0 → size p ≤ size q) ↔ irreducible_poly p.

End NonZero.
@@ -1159,7 +1158,7 @@
Hypothesis irr_p : irreducible_poly p.
-Let nz_p : p != 0.
+Let nz_p : p != 0.

@@ -1168,13 +1167,13 @@ The Vector axiom requires irreducibility.
-Lemma min_subfx_vectAxiom : Vector.axiom (size p).-1 subfx_lmodType.
+Lemma min_subfx_vectAxiom : Vector.axiom (size p).-1 subfx_lmodType.

Definition SubfxVectMixin := VectMixin min_subfx_vectAxiom.
Definition SubfxVectType := VectType F subFExtend SubfxVectMixin.
-Definition SubfxFalgType := Eval simpl in [FalgType F of SubfxVectType].
-Definition SubFieldExtType := Eval simpl in [fieldExtType F of SubfxFalgType].
+Definition SubfxFalgType := Eval simpl in [FalgType F of SubfxVectType].
+Definition SubFieldExtType := Eval simpl in [fieldExtType F of SubfxFalgType].

End Irreducible.
@@ -1185,10 +1184,10 @@

-Lemma irredp_FAdjoin (F : fieldType) (p : {poly F}) :
-    irreducible_poly p →
-  {L : fieldExtType F & \dim {:L} = (size p).-1 &
-    {z | root (map_poly (in_alg L) p) z & <<1; z>>%VS = fullv}}.
+Lemma irredp_FAdjoin (F : fieldType) (p : {poly F}) :
+    irreducible_poly p →
+  {L : fieldExtType F & \dim {:L} = (size p).-1 &
+    {z | root (map_poly (in_alg L) p) z & <<1; z>>%VS = fullv}}.

@@ -1221,13 +1220,13 @@ have mul1: left_id L1 mul. move=> x; rewrite /mul L1K mul1r /toL modp_small ?rVpolyK // -Dn ltnS. by rewrite size_poly. have mulD: left_distributive mul +%R. - move=> x y z; apply: canLR (@rVpolyK _ ) _. + move=> x y z; apply: canLR rVpolyK _. by rewrite !raddfD mulrDl /= !toL_K /toL modp_add. -have nzL1: L1 != 0 by rewrite -(can_eq (@rVpolyK _ )) L1K raddf0 oner_eq0. +have nzL1: L1 != 0 by rewrite -(can_eq rVpolyK) L1K raddf0 oner_eq0. pose mulM := ComRingMixin mulA mulC mul1 mulD nzL1. pose rL := ComRingType (RingType vL mulM) mulC. have mulZl: GRing.Lalgebra.axiom mul. - move=> a x y; apply: canRL (@rVpolyK _ ) _; rewrite !linearZ /= toL_K. + move=> a x y; apply: canRL rVpolyK _; rewrite !linearZ /= toL_K. by rewrite -scalerAl modp_scalel. have mulZr: @GRing.Algebra.axiom _ (LalgType F rL mulZl). by move=> a x y; rewrite !(mulrC x) scalerAl. @@ -1236,7 +1235,7 @@ pose uaL := [unitAlgType F of AlgType F urL mulZr]. pose faL := [FalgType F of uaL]. have unitE: GRing.Field.mixin_of urL. move=> x nz_x; apply/unitrP; set q := rVpoly x. - have nz_q: q != 0 by rewrite -(can_eq (@rVpolyK _ )) raddf0 in nz_x. + have nz_q: q != 0 by rewrite -(can_eq rVpolyK) raddf0 in nz_x. have /Bezout_eq1_coprimepP[u upq1]: coprimep p q. have /contraR := irr_p _ (dvdp_gcdl p q); apply. have: size (gcdp p q) <= size q by apply: leq_gcdpr. @@ -1256,12 +1255,11 @@ have q_z q: rVpoly (map_poly iota q). [z] = q %% p. rewrite linearZ /= L1K alg_polyC modp_add; congr (_ + _); last first. by rewrite modp_small // size_polyC; case: (~~ _) => //; apply: ltnW. by rewrite !toL_K IHq mulrC modp_mul mulrC modp_mul. -exists z; first by rewrite /root -(can_eq (@rVpolyK _ )) q_z modpp linear0. +exists z; first by rewrite /root -(can_eq rVpolyK) q_z modpp linear0. apply/vspaceP=> x; rewrite memvf; apply/Fadjoin_polyP. exists (map_poly iota (rVpoly x)). by apply/polyOverP=> i; rewrite coef_map memvZ ?mem1v. -apply: (can_inj (@rVpolyK _ )). -by rewrite q_z modp_small // -Dn ltnS size_poly. +by apply/(can_inj rVpolyK); rewrite q_z modp_small // -Dn ltnS size_poly. Qed. -- cgit v1.2.3