diff options
| author | Georges Gonthier | 2018-11-26 19:51:27 +0100 |
|---|---|---|
| committer | Georges Gonthier | 2018-11-26 19:51:27 +0100 |
| commit | 03ad994dfee48e1a7b2b7091c45dfdcf4402f826 (patch) | |
| tree | d891c2b8507452f2aaac1cbfe7dfbb709e751629 /mathcomp/field | |
| parent | add6e85884691faef1bf8742e803374815672cc2 (diff) | |
correct and improve signature and documentation of FieldMixin
Documentation of FieldUnitMixin and FieldMixin corrected to reflect
actual arguments, with mulVf and inv0 made explicit arguments for
FieldMixin (they were implicit due to the extended signature of
Field.mixin_of). Type of FieldMixin changed to a convertible variant to
facilitate construction of on-the-fly in-proof construction of
fieldType instances, exposing an idomainType instance.
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algC.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/closed_field.v | 4 |
2 files changed, 2 insertions, 4 deletions
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index aef136a..4b37a9c 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -377,7 +377,7 @@ Definition unitRingMixin := FieldUnitMixin mulVf inv0. Canonical unitRingType := UnitRingType type unitRingMixin. Canonical comUnitRingType := [comUnitRingType of type]. -Definition fieldMixin := @FieldMixin _ _ mulVf inv0. +Definition fieldMixin := FieldMixin mulVf inv0. Definition idomainAxiom := FieldIdomainMixin fieldMixin. Canonical idomainType := IdomainType type idomainAxiom. Canonical fieldType := FieldType type fieldMixin. diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index 1ae025b..ca738ef 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.v @@ -713,9 +713,7 @@ have EmulV: GRing.Field.axiom Einv. apply/eqP; case: sig_eqW => {ex_uv} [uv uv1]; set i := _.+1 in uv1 *. rewrite piE /= -[z]reprK -(rmorphM PtoE) -Quotient.idealrBE. by rewrite -uv1 opprD addNKr -mulNr; apply/memI; exists i; apply: dvdp_mull. -pose EringU := [comUnitRingType of UnitRingType _ (FieldUnitMixin EmulV Einv0)]. -have Eunitf := @FieldMixin _ _ EmulV Einv0. -pose Efield := FieldType (IdomainType EringU (FieldIdomainMixin Eunitf)) Eunitf. +pose Efield := FieldType _ (FieldMixin EmulV Einv0). pose Ecount := CountType Efield (CanCountMixin (@reprK _ _)). pose FtoE := [rmorphism of PtoE \o polyC]; pose w : E := PtoE 'X. have defPtoE q: (map_poly FtoE q).[w] = PtoE q. |