proposition: Lemma Minvl t u : \sum_(v : T) (Minv t v) * (M v u) = (u == t)%:R.
proof: Proof. rewrite (reindex _ (onW_bij _ (@enum_val_bij _))) /=. transitivity (mulmx (invmx Mat) Mat (enum_rank t) (enum_rank u)). rewrite mxE; apply eq_bigr => /= i _. by rewrite /Minv mxE enum_rankK enum_valK. rewrite mulVmx; last by rewrite unitmxE det_unitrig unitr1. rewrite mxE; congr (nat_of_bool _)%:R. by apply/eqP/eqP => [/(can_inj (@enum_rankK _))|] ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)