Enriched numClosedFieldType so that it factors a lot of theory from both complex and algC.

The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory
have been moved to the numClosedFieldType structure in ssrnum.
This covers boths the uses in algC and complex.v. To that end the
numClosedFieldType structure has been enriched with conjugation and 'i.
Note that 'i can be deduced from the property of algebraic closure and is
only here to let the user chose which definitional equality should hold
on 'i. Same thing for conjC that could be written  `|x|^+2/x, the only
nontrivial (up to my knowledge) property is the fact that conjugation
is a ring morphism.

2 files changed, 9 insertions, 8 deletions

diff --git a/mathcomp/character/all_character.v b/mathcomp/character/all_character.v
index 936fa6c..03f1b57 100644
--- a/mathcomp/character/all_character.v
+++ b/mathcomp/character/all_character.v
@@ -1,7 +1,7 @@
-Require Export character.
-Require Export classfun.
-Require Export inertia.
-Require Export integral_char.
-Require Export mxabelem.
-Require Export mxrepresentation.
-Require Export vcharacter.
+From mathcomp Require Export character.
+From mathcomp Require Export classfun.
+From mathcomp Require Export inertia.
+From mathcomp Require Export integral_char.
+From mathcomp Require Export mxabelem.
+From mathcomp Require Export mxrepresentation.
+From mathcomp Require Export vcharacter.
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 4c27bd7..7473338 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -969,7 +969,8 @@ Lemma cfCauchySchwarz_sqrt phi psi :
   `|'[phi, psi]| <= sqrtC '[phi] * sqrtC '[psi] ?= iff ~~ free (phi :: psi).
 Proof.
 rewrite -(sqrCK (normr_ge0 _)) -sqrtCM ?qualifE ?cfnorm_ge0 //.
-rewrite (mono_in_lerif ler_sqrtC) 1?rpredM ?qualifE ?normr_ge0 ?cfnorm_ge0 //.
+rewrite (mono_in_lerif (@ler_sqrtC _)) 1?rpredM ?qualifE;
+rewrite ?normr_ge0 ?cfnorm_ge0 //.
 exact: cfCauchySchwarz.
 Qed.