proposition: Lemma Minv_lincombl (Mod : lmodType R) (F G : T -> Mod) : (forall t, F t = \sum_u M t u *: G u) -> (forall t, G t = \sum_u Minv t u *: F u).
proof: Proof. move=> H t. under eq_bigr do [rewrite H scaler_sumr; under eq_bigr do rewrite scalerA]. rewrite exchange_big /= (bigD1 t) //= -scaler_suml Minvl eq_refl scale1r. rewrite big1 ?addr0 // => i /negbTE Hi. by rewrite -scaler_suml Minvl Hi scale0r. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)