chore(linear_algebra/determinant): Move some lemmas about swaps to be…

…tter files (#5201)

These lemmas are not specific to determinants, and I need them in another file imported by `determinant`.

src/data/equiv/basic.lean

@@ -1485,7 +1485,7 @@ lemma swap_eq_update (i j : α) :
   ⇑(equiv.swap i j) = update (update id j i) i j :=
 funext $ λ x, by rw [update_apply _ i j, update_apply _ j i, equiv.swap_apply_def, id.def]
 
-lemma comp_swap_eq_update {β : Type*} (i j : α) (f : α → β) :
+lemma comp_swap_eq_update (i j : α) (f : α → β) :
   f ∘ equiv.swap i j = update (update f j (f i)) i (f j) :=
 by rw [swap_eq_update, comp_update, comp_update, comp.right_id]
 
@@ -1498,10 +1498,18 @@ equiv.ext (λ x, begin
   split_ifs; simp
 end)
 
-@[simp] lemma swap_apply_self {α : Type*} [decidable_eq α] (i j a : α) :
+@[simp] lemma swap_apply_self (i j a : α) :
   swap i j (swap i j a) = a :=
 by rw [← equiv.trans_apply, equiv.swap_swap, equiv.refl_apply]
 
+/-- A function is invariant to a swap if it is equal at both elements -/
+lemma apply_swap_eq_self {v : α → β} {i j : α} (hv : v i = v j) (k : α) : v (swap i j k) = v k :=
+begin
+  by_cases hi : k = i, { rw [hi, swap_apply_left, hv] },
+  by_cases hj : k = j, { rw [hj, swap_apply_right, hv] },
+  rw swap_apply_of_ne_of_ne hi hj,
+end
+
 /-- Augment an equivalence with a prescribed mapping `f a = b` -/
 def set_value (f : α ≃ β) (a : α) (b : β) : α ≃ β :=
 (swap a (f.symm b)).trans f

src/group_theory/perm/sign.lean

@@ -27,6 +27,21 @@ variables {α : Type u} {β : Type v}
 
 namespace equiv.perm
 
+/--
+`mod_swap i j` contains permutations up to swapping `i` and `j`.
+
+We use this to partition permutations in `matrix.det_zero_of_row_eq`, such that each partition
+sums up to `0`.
+-/
+def mod_swap [decidable_eq α] (i j : α) : setoid (perm α) :=
+⟨λ σ τ, σ = τ ∨ σ = swap i j * τ,
+ λ σ, or.inl (refl σ),
+ λ σ τ h, or.cases_on h (λ h, or.inl h.symm) (λ h, or.inr (by rw [h, swap_mul_self_mul])),
+ λ σ τ υ hστ hτυ, by cases hστ; cases hτυ; try {rw [hστ, hτυ, swap_mul_self_mul]}; finish⟩
+
+instance {α : Type*} [fintype α] [decidable_eq α] (i j : α) : decidable_rel (mod_swap i j).r :=
+λ σ τ, or.decidable
+
 /-- If the permutation `f` fixes the subtype `{x // p x}`, then this returns the permutation
   on `{x // p x}` induced by `f`. -/
 def subtype_perm (f : perm α) {p : α → Prop} (h : ∀ x, p x ↔ p (f x)) : perm {x // p x} :=

src/linear_algebra/determinant.lean

@@ -184,33 +184,11 @@ end
 lemma det_eq_zero_of_column_eq_zero {A : matrix n n R} (j : n) (h : ∀ i, A i j = 0) : det A = 0 :=
 by { rw ← det_transpose, exact det_eq_zero_of_row_eq_zero j h, }
 
-/--
-  `mod_swap i j` contains permutations up to swapping `i` and `j`.
-
-  We use this to partition permutations in the expression for the determinant,
-  such that each partitions sums up to `0`.
--/
-def mod_swap {n : Type u} [decidable_eq n] (i j : n) : setoid (perm n) :=
-⟨ λ σ τ, σ = τ ∨ σ = swap i j * τ,
-  λ σ, or.inl (refl σ),
-  λ σ τ h, or.cases_on h (λ h, or.inl h.symm) (λ h, or.inr (by rw [h, swap_mul_self_mul])),
-  λ σ τ υ hστ hτυ, by cases hστ; cases hτυ; try {rw [hστ, hτυ, swap_mul_self_mul]}; finish⟩
-
-instance (i j : n) : decidable_rel (mod_swap i j).r := λ σ τ, or.decidable
-
 variables {M : matrix n n R} {i j : n}
 
 /-- If a matrix has a repeated row, the determinant will be zero. -/
 theorem det_zero_of_row_eq (i_ne_j : i ≠ j) (hij : M i = M j) : M.det = 0 :=
 begin
-  have swap_invariant : ∀ k, M (swap i j k) = M k,
-  { intros k,
-    rw [swap_apply_def],
-    by_cases k = i, { rw [if_pos h, h, ←hij] },
-    rw [if_neg h],
-    by_cases k = j, { rw [if_pos h, h, hij] },
-    rw [if_neg h] },
-
   have : ∀ σ, _root_.disjoint {σ} {swap i j * σ},
   { intros σ,
     rw [disjoint_singleton, mem_singleton],
@@ -224,7 +202,7 @@ begin
   rw [neg_mul_eq_neg_mul],
   congr,
   { rw [sign_mul, sign_swap i_ne_j], norm_num },
-  ext j, rw [perm.mul_apply, swap_invariant]
+  ext j, rw [perm.mul_apply, apply_swap_eq_self hij]
 end
 
 end det_zero