diff options
| author | affeldt-aist | 2020-11-20 12:41:11 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-20 12:41:11 +0900 |
| commit | 3bb1ccc63170e3e71ef9d5b62758b6fdb1c4371c (patch) | |
| tree | 076b8d8c53eaaf424258388bbd0068970c55b85f /mathcomp/character/character.v | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
| parent | e565f8d9bebd4fd681c34086d5448dbaebc11976 (diff) | |
Merge pull request #658 from CohenCyril/duplicate_clear
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/character/character.v')
| -rw-r--r-- | mathcomp/character/character.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index e7ea1e0..58a3688 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -1490,7 +1490,7 @@ Proof. move=> Gx; have [e [[B uB def_x] [_ e1] [-> _] _]] := repr_rsim_diag rG Gx. rewrite cfRepr1 -[n in n%:R]card_ord -sumr_const -(eq_bigr _ (in1W e1)). case/normC_sum_eq1=> [i _ | c /eqP norm_c_1 def_e]; first by rewrite e1. -have{def_e} def_e: e = const_mx c by apply/rowP=> i; rewrite mxE def_e ?andbT. +have{} def_e: e = const_mx c by apply/rowP=> i; rewrite mxE def_e ?andbT. by exists c => //; rewrite def_x def_e diag_const_mx scalar_mxC mulmxKV. Qed. @@ -1619,7 +1619,7 @@ apply: andb_id2l => Gx; rewrite {1 2}[chi]cfun_sum_constt !sum_cfunE. apply/eqP/bigcapP=> [Kx i Ci | Kx]; last first. by apply: eq_bigr => i /Kx Kx_i; rewrite !cfunE cfker1. rewrite cfkerEirr inE /= -(inj_eq (mulfI Ci)). -have:= (normC_sum_upper _ Kx) i; rewrite !cfunE => -> // {i Ci} i _. +have:= (normC_sum_upper _ Kx) i; rewrite !cfunE => -> // {Ci}i _. have chi_i_ge0: 0 <= '[chi, 'chi_i]. by rewrite Cnat_ge0 ?Cnat_cfdot_char_irr. by rewrite !cfunE normrM (normr_idP _) ?ler_wpmul2l ?char1_ge_norm ?irr_char. |