diff options
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/all_character.v | 14 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 3 |
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. |