proposition: Lemma alternate_determinant : forall n (A : 'M_n) i1 i2, i1 != i2 -> A i1 === A i2 -> \det A === 0.
proof: Proof. move=> n A i1 i2 Di12 A12; pose r := 'I_n. pose t := tperm i1 i2; pose tr s := (t * s)%g. have trK : involutive tr by move=> s; rewrite /tr mulgA tperm2 mul1g. rewrite /(\det _). setoid_rewrite (bigID (index_enum (perm_for_finType (ordinal_finType n))) (fun s => (s : bool))) => /=. set S1 := reducebig _ _ _ _ _; set T := S1 + _. have: req (S1 + (- S1)) 0 by ring. move => eq; rewrite <- eq; clear eq. apply radd_morph; first by reflexivity. rewrite {T}/S1. setoid_rewrite (big_morph (op2:=radd) (idx2:=0) (phi:=ropp)); [|by move=> x y; ring|by ring|by apply radd_morph]. setoid_rewrite (reindex (h:=tr)) at 1 => /=; last by exists tr => ? _. symmetry; apply eq_big => [s | s seven]. by rewrite /tr odd_permM odd_tperm Di12 negbK. rewrite odd_permM odd_tperm Di12 seven=> /=; ring_simplify. setoid_rewrite (reindex (h:=t)) at 1=>/=; last by exists (t : _ -> _) => i _; exact: tpermK. apply eq_bigr => i _; rewrite permM /t. by case: tpermP=> [H|H|H1 H2]; [rewrite -> H, (A12 _)|rewrite -> H, (A12 _)|]; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms