diff options
| author | Cyril Cohen | 2020-09-01 15:44:13 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-03 19:59:28 +0200 |
| commit | fbeec199e65fe7e9fd96ddd74e31aa0461c22927 (patch) | |
| tree | bff3b089214e20c21a63b053670793a7bf44fe91 /mathcomp/character | |
| parent | 495919767802fea4089594726d585c9b5305df21 (diff) | |
Lemmas reindex_omap and bigD1_ord
+ eq_liftF and lift_eqF
+ proof simplificaions
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/character.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 113ef8b..e7ea1e0 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -722,7 +722,7 @@ Lemma irr_free : free (irr G). Proof. apply/freeP=> s s0 i; apply: (mulIf (irr1_neq0 i)). rewrite mul0r -(raddf0 (xcfun_r_additive 'e_i)) -{}s0 raddf_sum /=. -rewrite (bigD1 i) //= -tnth_nth xcfunZl xcfun_id eqxx big1 ?addr0 // => j ne_ji. +rewrite (bigD1 i)//= -tnth_nth xcfunZl xcfun_id eqxx big1 ?addr0 // => j ne_ji. by rewrite -tnth_nth xcfunZl xcfun_id (negbTE ne_ji) mulr0. Qed. |