From fbeec199e65fe7e9fd96ddd74e31aa0461c22927 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 1 Sep 2020 15:44:13 +0200
Subject: Lemmas reindex_omap and bigD1_ord

+ eq_liftF and lift_eqF
+ proof simplificaions
---
 mathcomp/character/character.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/character')

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.
 
-- 
cgit v1.2.3