diff options
| author | Laurent Théry | 2020-09-04 12:14:00 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-04 12:14:00 +0200 |
| commit | d693784678f8a1889fdc3731587f31dc7c9377ff (patch) | |
| tree | 413e131d444270f9d993437f13122e4aa5bc4277 /mathcomp/character | |
| parent | 495919767802fea4089594726d585c9b5305df21 (diff) | |
| parent | 667dd52bd039a96f896b81533b0aaafe98b9f8de (diff) | |
Merge pull request #572 from CohenCyril/reindex_omap
Lemmas reindex_omap and bigD1_ord
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. |