diff options
| author | Georges Gonthier | 2015-12-01 09:43:02 +0000 |
|---|---|---|
| committer | Georges Gonthier | 2015-12-04 15:07:18 +0000 |
| commit | efc830f03047c94b386ea4b356717bd128906014 (patch) | |
| tree | efcd2861a5bf4a33222903acc72d879765c66a7c /mathcomp/field/falgebra.v | |
| parent | bd8cf1baa6758fef61ba8bd9917dc16bd6150613 (diff) | |
Add instances & lemmas for regular algebras
Diffstat (limited to 'mathcomp/field/falgebra.v')
| -rw-r--r-- | mathcomp/field/falgebra.v | 5 |
1 files changed, 5 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). |