From 03ad994dfee48e1a7b2b7091c45dfdcf4402f826 Mon Sep 17 00:00:00 2001 From: Georges Gonthier Date: Mon, 26 Nov 2018 19:51:27 +0100 Subject: 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. --- mathcomp/field/algC.v | 2 +- mathcomp/field/closed_field.v | 4 +--- 2 files changed, 2 insertions(+), 4 deletions(-) (limited to 'mathcomp/field') 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. -- cgit v1.2.3