Add instances & lemmas for regular algebras

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).