diff options
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algC.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index 6c53127..cbcbc3a 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -445,8 +445,8 @@ rewrite -(fmorph_root CtoL_rmorphism) -map_poly_comp; congr (root _ _): pu0. by apply/esym/eq_map_poly; apply: fmorph_eq_rat. Qed. -Program Definition conjMixin := - ImaginaryMixin (svalP (imaginary_exists closedFieldType)) +Definition conjMixin := + ImaginaryMixin (svalP (imaginary_exists closedFieldType)) (fun x => esym (normK x)). Canonical numClosedFieldType := NumClosedFieldType type conjMixin. |