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 | |
| parent | 8150209d2aaa0034b3dca9d82be1aeb11a12b5ea (diff) | |
Fixed inheritance of fieldExt / fieldOver / splitting field
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/fieldext.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/galois.v | 6 |
2 files changed, 9 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. diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index 30bef47..9a2bdfd 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.v @@ -370,6 +370,8 @@ Definition lmodType := @Lmodule.Pack F phF cT xclass. Definition lalgType := @Lalgebra.Pack F phF cT xclass. Definition algType := @Algebra.Pack F phF cT xclass. Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass. +Definition comAlgType := @ComAlgebra.Pack F phF cT xclass. +Definition comUnitAlgType := @ComUnitAlgebra.Pack F phF cT xclass. Definition vectType := @Vector.Pack F phF cT xclass. Definition FalgType := @Falgebra.Pack F phF cT xclass. Definition fieldExtType := @FieldExt.Pack F phF cT xclass. @@ -405,8 +407,12 @@ Coercion lalgType : type >-> Lalgebra.type. Canonical lalgType. Coercion algType : type >-> Algebra.type. Canonical algType. +Coercion comAlgType : type >-> ComAlgebra.type. +Canonical comAlgType. Coercion unitAlgType : type >-> UnitAlgebra.type. Canonical unitAlgType. +Coercion comUnitAlgType : type >-> ComUnitAlgebra.type. +Canonical comUnitAlgType. Coercion vectType : type >-> Vector.type. Canonical vectType. Coercion FalgType : type >-> Falgebra.type. |