proposition: Lemma determinant_alternate n (A : 'M[R]_n) i1 i2 : i1 != i2 -> A i1 =1 A i2 -> \det A = 0.
proof: Proof. move=> neq_i12 eqA12; pose t := tperm i1 i2. have oddMt s: (t * s)%g = ~~ s :> bool by rewrite odd_permM odd_tperm neq_i12. rewrite [\det A](bigID (@odd_perm _)) /=. apply: canLR (subrK _) _; rewrite add0r -sumrN. rewrite (reindex_inj (mulgI t)); apply: eq_big => //= s. rewrite oddMt => /negPf->; rewrite mulN1r mul1r; congr (- _). rewrite (reindex_perm t); apply: eq_bigr => /= i _. by rewrite permM tpermK /t; case: tpermP => // ->; rewrite eqA12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)