diff options
| author | Florent Hivert | 2019-11-04 13:42:59 +0100 |
|---|---|---|
| committer | Florent Hivert | 2019-11-04 13:42:59 +0100 |
| commit | 6ba0e77cd7f8d68647790fe2b704f35ae76ad1f8 (patch) | |
| tree | b84a0bbb76b0a89b17b84fd7d364814dfe7b7a75 /mathcomp/field/fieldext.v | |
| parent | 8150209d2aaa0034b3dca9d82be1aeb11a12b5ea (diff) | |
Fixed inheritance of fieldExt / fieldOver / splitting field
Diffstat (limited to 'mathcomp/field/fieldext.v')
| -rw-r--r-- | mathcomp/field/fieldext.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 3ecd00a..64239f3 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.v @@ -198,6 +198,7 @@ Coercion sort : type >-> Sortclass. Bind Scope ring_scope with sort. Coercion base : class_of >-> Falgebra.class_of. Coercion base4 : class_of >-> Field.class_of. +Coercion base6 : class_of >-> ComUnitAlgebra.class_of. Coercion eqType : type >-> Equality.type. Canonical eqType. Coercion choiceType : type >-> Choice.type. @@ -837,6 +838,8 @@ Proof. exact: mulrCA. Qed. Canonical fieldOver_algType := AlgType K_F L_F fieldOver_scaleAr. Canonical fieldOver_unitAlgType := [unitAlgType K_F of L_F]. +Canonical fieldOver_comAlgType := [comAlgType K_F of L_F]. +Canonical fieldOver_comUnitAlgType := [comUnitAlgType K_F of L_F]. Fact fieldOver_vectMixin : Vector.mixin_of fieldOver_lmodType. Proof. |