diff options
| -rw-r--r-- | mathcomp/field/falgebra.v | 5 | ||||
| -rw-r--r-- | mathcomp/field/fieldext.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 9 |
3 files changed, 16 insertions, 0 deletions
diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 8a9aaac..317819c 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.v @@ -214,6 +214,11 @@ Notation "1" := (vline 1) : vspace_scope. Canonical matrix_FalgType (K : fieldType) n := [FalgType K of 'M[K]_n.+1]. +Canonical regular_FalgType (R : comUnitRingType) := [FalgType R of R^o]. + +Lemma regular_fullv (K : fieldType) : (fullv = 1 :> {vspace K^o})%VS. +Proof. by apply/esym/eqP; rewrite eqEdim subvf dim_vline oner_eq0 dimvf. Qed. + Section Proper. Variables (R : ringType) (aT : FalgType R). diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 234ad47..5fefc49 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -265,6 +265,8 @@ End Exports. End FieldExt. Export FieldExt.Exports. +Canonical regular_fieldExtType (F : fieldType) := [fieldExtType F of F^o for F]. + Section FieldExtTheory. Variables (F0 : fieldType) (L : fieldExtType F0). diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index bb62912..2b8c382 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -456,6 +456,15 @@ apply/seqv_sub_adjoin/imageP; rewrite (tnth_nth 0) /in_mem/=. by exists (i, widen_ord (sz_r i) j) => /=. Qed. +Fact regular_splittingAxiom F : SplittingField.axiom (regular_fieldExtType F). +Proof. +exists 1; first exact: rpred1. +by exists [::]; [rewrite big_nil eqpxx | rewrite Fadjoin_nil regular_fullv]. +Qed. + +Canonical regular_splittingFieldType (F : fieldType) := + SplittingFieldType F F^o (regular_splittingAxiom F). + Section SplittingFieldTheory. Variables (F : fieldType) (L : splittingFieldType F). |