Exact source: Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
Pinned GitHub source · Raw UTF-8 source
Back to The satellite polynomial is linear in the maximal-minor vector
1/-2Copyright (c) 2018 Kenny Lau. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Kenny Lau, Chris Hughes, Anne Baanen5-/6module78public import Mathlib.Data.Matrix.Basic9public import Mathlib.Data.Matrix.Block10public import Mathlib.LinearAlgebra.Matrix.Notation11public import Mathlib.LinearAlgebra.Matrix.RowCol12public import Mathlib.GroupTheory.Perm.Fin13public import Mathlib.LinearAlgebra.Alternating.Basic14public import Mathlib.LinearAlgebra.Matrix.SemiringInverse1516/-!17# Determinant of a matrix1819This file defines the determinant of a matrix, `Matrix.det`, and its essential properties.2021## Main definitions2223- `Matrix.det`: the determinant of a square matrix, as a sum over permutations24- `Matrix.detRowAlternating`: the determinant, as an `AlternatingMap` in the rows of the matrix2526## Main results2728- `det_mul`: the determinant of `A * B` is the product of determinants29- `det_zero_of_row_eq`: the determinant is zero if there is a repeated row30- `det_block_diagonal`: the determinant of a block diagonal matrix is a product31 of the blocks' determinants3233## Implementation notes3435It is possible to configure `simp` to compute determinants. See the file36`MathlibTest/matrix.lean` for some examples.3738-/3940@[expose] public section414243universe u v w z4445open Equiv Equiv.Perm Finset Function4647namespace Matrix4849variable {m n : Type*} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m]50variable {R : Type v} [CommRing R]5152local notation "ε " σ:arg => ((sign σ : ℤ) : R)5354/-- `det` is an `AlternatingMap` in the rows of the matrix. -/55def detRowAlternating : (n → R) [⋀^n]→ₗ[R] R :=56 MultilinearMap.alternatization ((MultilinearMap.mkPiAlgebra R n R).compLinearMap LinearMap.proj)5758/-- The determinant of a matrix given by the Leibniz formula. -/59@[wikidata Q178546]60def det (M : Matrix n n R) : R :=61 detRowAlternating M6263theorem det_apply (M : Matrix n n R) : M.det = ∑ σ : Perm n, Equiv.Perm.sign σ • ∏ i, M (σ i) i :=64 MultilinearMap.alternatization_apply _ M6566-- This is what the old definition was. We use it to avoid having to change the old proofs below67theorem det_apply' (M : Matrix n n R) : M.det = ∑ σ : Perm n, ε σ * ∏ i, M (σ i) i := by68 simp [det_apply, Units.smul_def]6970theorem det_eq_detp_sub_detp (M : Matrix n n R) : M.det = M.detp 1 - M.detp (-1) := by71 rw [det_apply, ← Equiv.sum_comp (Equiv.inv (Perm n)), ← ofSign_disjUnion, sum_disjUnion]72 simp_rw [inv_apply, sign_inv, sub_eq_add_neg, detp, ← sum_neg_distrib]73 refine congr_arg₂ (· + ·) (sum_congr rfl fun σ hσ ↦ ?_) (sum_congr rfl fun σ hσ ↦ ?_) <;>74 rw [mem_ofSign.mp hσ, ← Equiv.prod_comp σ] <;> simp7576@[simp]77theorem det_diagonal {d : n → R} : det (diagonal d) = ∏ i, d i := by78 rw [det_apply']79 refine (Finset.sum_eq_single 1 ?_ ?_).trans ?_80 · rintro σ - h281 obtain ⟨x, h3⟩ := not_forall.1 (mt Equiv.ext h2)82 convert! mul_zero (ε σ)83 apply Finset.prod_eq_zero (mem_univ x)84 exact if_neg h385 · simp86 · simp8788theorem det_zero (_ : Nonempty n) : det (0 : Matrix n n R) = 0 :=89 (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_zero9091@[simp]92theorem det_one : det (1 : Matrix n n R) = 1 := by rw [← diagonal_one]; simp [-diagonal_one]9394theorem det_isEmpty [IsEmpty n] {A : Matrix n n R} : det A = 1 := by simp [det_apply]9596@[simp]97theorem coe_det_isEmpty [IsEmpty n] : (det : Matrix n n R → R) = Function.const _ 1 := by98 ext99 exact det_isEmpty100101theorem det_eq_one_of_card_eq_zero {A : Matrix n n R} (h : Fintype.card n = 0) : det A = 1 :=102 haveI : IsEmpty n := Fintype.card_eq_zero_iff.mp h103 det_isEmpty104105/-- If `n` has only one element, the determinant of an `n` by `n` matrix is just that element.106Although `Unique` implies `DecidableEq` and `Fintype`, the instances might107not be syntactically equal. Thus, we need to fill in the args explicitly. -/108@[simp]109theorem det_unique {n : Type*} [Unique n] [DecidableEq n] [Fintype n] (A : Matrix n n R) :110 det A = A default default := by simp [det_apply, univ_unique]111112theorem det_eq_elem_of_subsingleton [Subsingleton n] (A : Matrix n n R) (k : n) :113 det A = A k k := by114 have := uniqueOfSubsingleton k115 convert! det_unique A116117theorem det_eq_elem_of_card_eq_one {A : Matrix n n R} (h : Fintype.card n = 1) (k : n) :118 det A = A k k :=119 haveI : Subsingleton n := Fintype.card_le_one_iff_subsingleton.mp h.le120 det_eq_elem_of_subsingleton _ _121122theorem det_mul_aux {M N : Matrix n n R} {p : n → n} (H : ¬Bijective p) :123 (∑ σ : Perm n, ε σ * ∏ x, M (σ x) (p x) * N (p x) x) = 0 := by124 obtain ⟨i, j, hpij, hij⟩ : ∃ i j, p i = p j ∧ i ≠ j := by125 rw [← Finite.injective_iff_bijective, Injective] at H126 push Not at H127 exact H128 exact129 sum_involution (fun σ _ => σ * Equiv.swap i j)130 (fun σ _ => by131 have : (∏ x, M (σ x) (p x)) = ∏ x, M ((σ * Equiv.swap i j) x) (p x) :=132 Fintype.prod_equiv (swap i j) _ _ (by simp [apply_swap_eq_self hpij])133 simp [this, sign_swap hij, -sign_swap', prod_mul_distrib])134 (fun σ _ _ => (not_congr mul_swap_eq_iff).mpr hij) (fun _ _ => mem_univ _) fun σ _ =>135 mul_swap_involutive i j σ136137@[simp]138theorem det_mul (M N : Matrix n n R) : det (M * N) = det M * det N :=139 calc140 det (M * N) = ∑ p : n → n, ∑ σ : Perm n, ε σ * ∏ i, M (σ i) (p i) * N (p i) i := by141 simp only [det_apply', mul_apply, prod_univ_sum, mul_sum, Fintype.piFinset_univ]142 rw [Finset.sum_comm]143 _ = ∑ p : n → n with Bijective p, ∑ σ : Perm n, ε σ * ∏ i, M (σ i) (p i) * N (p i) i := by144 refine (sum_subset (filter_subset _ _) fun f _ hbij ↦ det_mul_aux ?_).symm145 simpa only [mem_filter_univ] using hbij146 _ = ∑ τ : Perm n, ∑ σ : Perm n, ε σ * ∏ i, M (σ i) (τ i) * N (τ i) i :=147 sum_bij (fun p h ↦ Equiv.ofBijective p (mem_filter.1 h).2) (fun _ _ ↦ mem_univ _)148 (fun _ _ _ _ h ↦ by injection h)149 (fun b _ ↦ ⟨b, mem_filter.2 ⟨mem_univ _, b.bijective⟩, coe_fn_injective rfl⟩) fun _ _ ↦ rfl150 _ = ∑ σ : Perm n, ∑ τ : Perm n, (∏ i, N (σ i) i) * ε τ * ∏ j, M (τ j) (σ j) := by151 simp only [mul_comm, mul_left_comm, prod_mul_distrib, mul_assoc]152 _ = ∑ σ : Perm n, ∑ τ : Perm n, (∏ i, N (σ i) i) * (ε σ * ε τ) * ∏ i, M (τ i) i :=153 (sum_congr rfl fun σ _ =>154 Fintype.sum_equiv (Equiv.mulRight σ⁻¹) _ _ fun τ => by155 have : (∏ j, M (τ j) (σ j)) = ∏ j, M ((τ * σ⁻¹) j) j := by156 rw [← (σ⁻¹ : _ ≃ _).prod_comp]157 simp158 have h : ε σ * ε (τ * σ⁻¹) = ε τ :=159 calc160 ε σ * ε (τ * σ⁻¹) = ε (τ * σ⁻¹ * σ) := by161 rw [mul_comm, sign_mul (τ * σ⁻¹)]162 simp only [Int.cast_mul, Units.val_mul]163 _ = ε τ := by simp only [inv_mul_cancel_right]164 simp_rw [Equiv.coe_mulRight, h]165 simp only [this])166 _ = det M * det N := by167 simp only [det_apply', Finset.mul_sum, mul_comm, mul_left_comm, mul_assoc]168169/-- The determinant of a matrix, as a monoid homomorphism. -/170def detMonoidHom : Matrix n n R →* R where171 toFun := det172 map_one' := det_one173 map_mul' := det_mul174175@[simp]176theorem coe_detMonoidHom : (detMonoidHom : Matrix n n R → R) = det :=177 rfl178179/-- On square matrices, `mul_comm` applies under `det`. -/180theorem det_mul_comm (M N : Matrix m m R) : det (M * N) = det (N * M) := by181 rw [det_mul, det_mul, mul_comm]182183/-- On square matrices, `mul_left_comm` applies under `det`. -/184theorem det_mul_left_comm (M N P : Matrix m m R) : det (M * (N * P)) = det (N * (M * P)) := by185 rw [← Matrix.mul_assoc, ← Matrix.mul_assoc, det_mul, det_mul_comm M N, ← det_mul]186187/-- On square matrices, `mul_right_comm` applies under `det`. -/188theorem det_mul_right_comm (M N P : Matrix m m R) : det (M * N * P) = det (M * P * N) := by189 rw [Matrix.mul_assoc, Matrix.mul_assoc, det_mul, det_mul_comm N P, ← det_mul]190191-- TODO(https://github.com/leanprover-community/mathlib4/issues/6607): fix elaboration so `val` isn't needed192theorem det_units_conj (M : (Matrix m m R)ˣ) (N : Matrix m m R) :193 det (M.val * N * M⁻¹.val) = det N := by194 rw [det_mul_right_comm, Units.mul_inv, one_mul]195196-- TODO(https://github.com/leanprover-community/mathlib4/issues/6607): fix elaboration so `val` isn't needed197theorem det_units_conj' (M : (Matrix m m R)ˣ) (N : Matrix m m R) :198 det (M⁻¹.val * N * ↑M.val) = det N :=199 det_units_conj M⁻¹ N200201/-- Transposing a matrix preserves the determinant. -/202@[simp]203theorem det_transpose (M : Matrix n n R) : Mᵀ.det = M.det := by204 rw [det_apply', det_apply']205 refine Fintype.sum_bijective _ inv_involutive.bijective _ _ ?_206 intro σ207 rw [sign_inv]208 congr 1209 apply Fintype.prod_equiv σ210 simp211212/-- Permuting the columns changes the sign of the determinant. -/213theorem det_permute (σ : Perm n) (M : Matrix n n R) :214 (M.submatrix σ id).det = Perm.sign σ * M.det :=215 ((detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_perm M σ).trans (by simp [Units.smul_def, det])216217/-- Permuting the rows changes the sign of the determinant. -/218theorem det_permute' (σ : Perm n) (M : Matrix n n R) :219 (M.submatrix id σ).det = Perm.sign σ * M.det := by220 rw [← det_transpose, transpose_submatrix, det_permute, det_transpose]221222/-- Permuting rows and columns with the same equivalence does not change the determinant. -/223@[simp]224theorem det_submatrix_equiv_self (e : n ≃ m) (A : Matrix m m R) :225 det (A.submatrix e e) = det A := by226 rw [det_apply', det_apply']227 apply Fintype.sum_equiv (Equiv.permCongr e)228 intro σ229 rw [Equiv.Perm.sign_permCongr e σ]230 congr 1231 apply Fintype.prod_equiv e232 intro i233 rw [Equiv.permCongr_apply, Equiv.symm_apply_apply, submatrix_apply]234235/-- Permuting rows and columns with two equivalences does not change the absolute value of the236determinant. -/237@[simp]238theorem abs_det_submatrix_equiv_equiv {R : Type*}239 [CommRing R] [LinearOrder R] [IsStrictOrderedRing R]240 (e₁ e₂ : n ≃ m) (A : Matrix m m R) :241 |(A.submatrix e₁ e₂).det| = |A.det| := by242 have hee : e₂ = e₁.trans (e₁.symm.trans e₂) := by ext; simp243 rw [hee]244 change |((A.submatrix id (e₁.symm.trans e₂)).submatrix e₁ e₁).det| = |A.det|245 rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]246247/-- Reindexing both indices along the same equivalence preserves the determinant.248249For the `simp` version of this lemma, see `det_submatrix_equiv_self`; this one is unsuitable because250`Matrix.reindex_apply` unfolds `reindex` first.251-/252theorem det_reindex_self (e : m ≃ n) (A : Matrix m m R) : det (reindex e e A) = det A :=253 det_submatrix_equiv_self e.symm A254255lemma det_reindex (e e' : m ≃ n) (M : Matrix m m R) :256 (M.reindex e e').det = sign (e'.trans e.symm) * M.det := by257 trans ((M.reindex (e.trans e'.symm) (.refl _)).reindex e' e').det258 · congr 1; ext; simp259 · simp_rw [det_reindex_self, reindex_apply, Equiv.refl_symm, Equiv.coe_refl, det_permute]260 rfl261262/-- Reindexing both indices along equivalences preserves the absolute of the determinant.263264For the `simp` version of this lemma, see `abs_det_submatrix_equiv_equiv`;265this one is unsuitable because `Matrix.reindex_apply` unfolds `reindex` first.266-/267theorem abs_det_reindex {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R]268 (e₁ e₂ : m ≃ n) (A : Matrix m m R) :269 |det (reindex e₁ e₂ A)| = |det A| :=270 abs_det_submatrix_equiv_equiv e₁.symm e₂.symm A271272theorem det_smul (A : Matrix n n R) (c : R) : det (c • A) = c ^ Fintype.card n * det A :=273 calc274 det (c • A) = det ((diagonal fun _ => c) * A) := by rw [smul_eq_diagonal_mul]275 _ = det (diagonal fun _ => c) * det A := det_mul _ _276 _ = c ^ Fintype.card n * det A := by simp277278@[simp]279theorem det_smul_of_tower {α} [Monoid α] [MulAction α R] [IsScalarTower α R R]280 [SMulCommClass α R R] (c : α) (A : Matrix n n R) :281 det (c • A) = c ^ Fintype.card n • det A := by282 rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]283284theorem det_neg (A : Matrix n n R) : det (-A) = (-1) ^ Fintype.card n * det A := by285 rw [← det_smul, neg_one_smul]286287/-- A variant of `Matrix.det_neg` with scalar multiplication by `Units ℤ` instead of multiplication288by `R`. -/289theorem det_neg_eq_smul (A : Matrix n n R) :290 det (-A) = (-1 : Units ℤ) ^ Fintype.card n • det A := by291 rw [← det_smul_of_tower, Units.neg_smul, one_smul]292293/-- Multiplying each row by a fixed `v i` multiplies the determinant by294the product of the `v`s. -/295theorem det_mul_row (v : n → R) (A : Matrix n n R) :296 det (of fun i j => v j * A i j) = (∏ i, v i) * det A :=297 calc298 det (of fun i j => v j * A i j) = det (A * diagonal v) :=299 congr_arg det <| by300 ext301 simp [mul_comm]302 _ = (∏ i, v i) * det A := by rw [det_mul, det_diagonal, mul_comm]303304/-- Multiplying each column by a fixed `v j` multiplies the determinant by305the product of the `v`s. -/306theorem det_mul_column (v : n → R) (A : Matrix n n R) :307 det (of fun i j => v i * A i j) = (∏ i, v i) * det A :=308 MultilinearMap.map_smul_univ _ v A309310@[simp]311theorem det_pow (M : Matrix m m R) (n : ℕ) : det (M ^ n) = det M ^ n :=312 (detMonoidHom : Matrix m m R →* R).map_pow M n313314section HomMap315316variable {S : Type w} [CommRing S]317318theorem _root_.RingHom.map_det (f : R →+* S) (M : Matrix n n R) :319 f M.det = Matrix.det (f.mapMatrix M) := by320 simp [Matrix.det_apply', map_sum f, map_prod f]321322theorem _root_.RingEquiv.map_det (f : R ≃+* S) (M : Matrix n n R) :323 f M.det = Matrix.det (f.mapMatrix M) :=324 f.toRingHom.map_det _325326theorem _root_.AlgHom.map_det [Algebra R S] {T : Type z} [CommRing T] [Algebra R T] (f : S →ₐ[R] T)327 (M : Matrix n n S) : f M.det = Matrix.det (f.mapMatrix M) :=328 f.toRingHom.map_det _329330theorem _root_.AlgEquiv.map_det [Algebra R S] {T : Type z} [CommRing T] [Algebra R T]331 (f : S ≃ₐ[R] T) (M : Matrix n n S) : f M.det = Matrix.det (f.mapMatrix M) :=332 f.toAlgHom.map_det _333334@[norm_cast]335theorem _root_.Int.cast_det (M : Matrix n n ℤ) :336 (M.det : R) = (M.map fun x ↦ (x : R)).det :=337 Int.castRingHom R |>.map_det M338339@[norm_cast]340theorem _root_.Rat.cast_det {F : Type*} [Field F] [CharZero F] (M : Matrix n n ℚ) :341 (M.det : F) = (M.map fun x ↦ (x : F)).det :=342 Rat.castHom F |>.map_det M343344end HomMap345346@[simp]347theorem det_conjTranspose [StarRing R] (M : Matrix m m R) : det Mᴴ = star (det M) :=348 ((starRingEnd R).map_det _).symm.trans <| congr_arg star M.det_transpose349350section DetZero351352/-!353### `det_zero` section354355Prove that a matrix with a repeated column has determinant equal to zero.356-/357358359theorem det_eq_zero_of_row_eq_zero {A : Matrix n n R} (i : n) (h : ∀ j, A i j = 0) : det A = 0 :=360 (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_coord_zero i (funext h)361362theorem det_eq_zero_of_column_eq_zero {A : Matrix n n R} (j : n) (h : ∀ i, A i j = 0) :363 det A = 0 := by364 rw [← det_transpose]365 exact det_eq_zero_of_row_eq_zero j h366367variable {M : Matrix n n R} {i j : n}368369/-- If a matrix has a repeated row, the determinant will be zero. -/370theorem det_zero_of_row_eq (i_ne_j : i ≠ j) (hij : M i = M j) : M.det = 0 :=371 (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_eq_zero_of_eq M hij i_ne_j372373/-- If a matrix has a repeated column, the determinant will be zero. -/374theorem det_zero_of_column_eq (i_ne_j : i ≠ j) (hij : ∀ k, M k i = M k j) : M.det = 0 := by375 rw [← det_transpose, det_zero_of_row_eq i_ne_j]376 exact funext hij377378/-- If we repeat a row of a matrix, we get a matrix of determinant zero. -/379theorem det_updateRow_eq_zero (h : i ≠ j) :380 (M.updateRow j (M i)).det = 0 := det_zero_of_row_eq h (by simp [h])381382/-- If we repeat a column of a matrix, we get a matrix of determinant zero. -/383theorem det_updateCol_eq_zero (h : i ≠ j) :384 (M.updateCol j (fun k ↦ M k i)).det = 0 := det_zero_of_column_eq h (by simp [h])385386end DetZero387388theorem det_updateRow_add (M : Matrix n n R) (j : n) (u v : n → R) :389 det (updateRow M j <| u + v) = det (updateRow M j u) + det (updateRow M j v) :=390 (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_update_add M j u v391392theorem det_updateCol_add (M : Matrix n n R) (j : n) (u v : n → R) :393 det (updateCol M j <| u + v) = det (updateCol M j u) + det (updateCol M j v) := by394 rw [← det_transpose, ← updateRow_transpose, det_updateRow_add]395 simp [updateRow_transpose, det_transpose]396397theorem det_updateRow_smul (M : Matrix n n R) (j : n) (s : R) (u : n → R) :398 det (updateRow M j <| s • u) = s * det (updateRow M j u) :=399 (detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_update_smul M j s u400401theorem det_updateCol_smul (M : Matrix n n R) (j : n) (s : R) (u : n → R) :402 det (updateCol M j <| s • u) = s * det (updateCol M j u) := by403 rw [← det_transpose, ← updateRow_transpose, det_updateRow_smul]404 simp [updateRow_transpose, det_transpose]405406theorem det_updateRow_smul_left (M : Matrix n n R) (j : n) (s : R) (u : n → R) :407 det (updateRow (s • M) j u) = s ^ (Fintype.card n - 1) * det (updateRow M j u) :=408 MultilinearMap.map_update_smul_left _ M j s u409410theorem det_updateCol_smul_left (M : Matrix n n R) (j : n) (s : R) (u : n → R) :411 det (updateCol (s • M) j u) = s ^ (Fintype.card n - 1) * det (updateCol M j u) := by412 rw [← det_transpose, ← updateRow_transpose, transpose_smul, det_updateRow_smul_left]413 simp [updateRow_transpose, det_transpose]414415theorem det_updateRow_sum_aux (M : Matrix n n R) {j : n} (s : Finset n) (hj : j ∉ s) (c : n → R)416 (a : R) :417 (M.updateRow j (a • M j + ∑ k ∈ s, (c k) • M k)).det = a • M.det := by418 induction s using Finset.induction_on with419 | empty => rw [Finset.sum_empty, add_zero, smul_eq_mul, det_updateRow_smul, updateRow_eq_self]420 | insert k _ hk h_ind =>421 have h : k ≠ j := fun h ↦ (h ▸ hj) (Finset.mem_insert_self _ _)422 rw [Finset.sum_insert hk, add_comm ((c k) • M k), ← add_assoc, det_updateRow_add,423 det_updateRow_smul, det_updateRow_eq_zero h, mul_zero, add_zero, h_ind]424 exact fun h ↦ hj (Finset.mem_insert_of_mem h)425426/-- If we replace a row of a matrix by a linear combination of its rows, then the determinant is427multiplied by the coefficient of that row. -/428theorem det_updateRow_sum (A : Matrix n n R) (j : n) (c : n → R) :429 (A.updateRow j (∑ k, (c k) • A k)).det = (c j) • A.det := by430 convert! det_updateRow_sum_aux A (Finset.univ.erase j) (Finset.univ.notMem_erase j) c (c j)431 rw [← Finset.univ.add_sum_erase _ (Finset.mem_univ j)]432433/-- If we replace a column of a matrix by a linear combination of its columns, then the determinant434is multiplied by the coefficient of that column. -/435theorem det_updateCol_sum (A : Matrix n n R) (j : n) (c : n → R) :436 (A.updateCol j (fun k ↦ ∑ i, (c i) • A k i)).det = (c j) • A.det := by437 rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]438 convert! det_updateRow_sum A.transpose j c439 simp only [smul_eq_mul, Finset.sum_apply, Pi.smul_apply, transpose_apply]440441section DetEq442443/-! ### `det_eq` section444445Lemmas showing the determinant is invariant under a variety of operations.446-/447448449theorem det_eq_of_eq_mul_det_one {A B : Matrix n n R} (C : Matrix n n R) (hC : det C = 1)450 (hA : A = B * C) : det A = det B :=451 calc452 det A = det (B * C) := congr_arg _ hA453 _ = det B * det C := det_mul _ _454 _ = det B := by rw [hC, mul_one]455456theorem det_eq_of_eq_det_one_mul {A B : Matrix n n R} (C : Matrix n n R) (hC : det C = 1)457 (hA : A = C * B) : det A = det B :=458 calc459 det A = det (C * B) := congr_arg _ hA460 _ = det C * det B := det_mul _ _461 _ = det B := by rw [hC, one_mul]462463theorem det_updateRow_add_self (A : Matrix n n R) {i j : n} (hij : i ≠ j) :464 det (updateRow A i (A i + A j)) = det A := by465 simp [det_updateRow_add,466 det_zero_of_row_eq hij (updateRow_self.trans (updateRow_ne hij.symm).symm)]467468theorem det_updateCol_add_self (A : Matrix n n R) {i j : n} (hij : i ≠ j) :469 det (updateCol A i fun k => A k i + A k j) = det A := by470 rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]471 exact det_updateRow_add_self Aᵀ hij472473theorem det_updateRow_add_smul_self (A : Matrix n n R) {i j : n} (hij : i ≠ j) (c : R) :474 det (updateRow A i (A i + c • A j)) = det A := by475 simp [det_updateRow_add, det_updateRow_smul,476 det_zero_of_row_eq hij (updateRow_self.trans (updateRow_ne hij.symm).symm)]477478theorem det_updateCol_add_smul_self (A : Matrix n n R) {i j : n} (hij : i ≠ j) (c : R) :479 det (updateCol A i fun k => A k i + c • A k j) = det A := by480 rw [← det_transpose, ← updateRow_transpose, ← det_transpose A]481 exact det_updateRow_add_smul_self Aᵀ hij c482483theorem det_eq_zero_of_not_linearIndependent_rows [IsDomain R] {A : Matrix m m R}484 (hA : ¬ LinearIndependent R (fun i ↦ A i)) :485 det A = 0 := detRowAlternating.map_linearDependent A hA486487theorem linearIndependent_rows_of_det_ne_zero [IsDomain R] {A : Matrix m m R} (hA : A.det ≠ 0) :488 LinearIndependent R (fun i ↦ A i) := by489 contrapose hA490 exact det_eq_zero_of_not_linearIndependent_rows hA491492theorem linearIndependent_cols_of_det_ne_zero [IsDomain R] {A : Matrix m m R} (hA : A.det ≠ 0) :493 LinearIndependent R A.col :=494 Matrix.linearIndependent_rows_of_det_ne_zero (by simpa [Matrix.col])495496theorem det_eq_zero_of_not_linearIndependent_cols [IsDomain R] {A : Matrix m m R}497 (hA : ¬ LinearIndependent R (fun i ↦ Aᵀ i)) :498 det A = 0 := by499 contrapose! hA500 exact linearIndependent_cols_of_det_ne_zero hA501502theorem det_vecMulVec [Nontrivial n] (u v : n → R) : (vecMulVec u v).det = 0 := by503 obtain ⟨i, j, hij⟩ := exists_pair_ne n504 let uv' := ((vecMulVec u v).updateRow i v).updateRow j v505 have huv' : uv'.det = 0 := by506 refine detRowAlternating.map_eq_zero_of_eq _ ?_ hij507 simp [uv', hij]508 have : vecMulVec u v =509 (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j) := by510 unfold uv'511 rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij,512 updateRow_self, updateRow_self, updateRow_comm _ hij, updateRow_idem,513 ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i, update_eq_self]514 rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv',515 mul_zero, mul_zero]516517theorem det_eq_of_forall_row_eq_smul_add_const_aux {A B : Matrix n n R} {s : Finset n} :518 ∀ (c : n → R) (_ : ∀ i, i ∉ s → c i = 0) (k : n) (_ : k ∉ s)519 (_ : ∀ i j, A i j = B i j + c i * B k j), det A = det B := by520 induction s using Finset.induction_on generalizing B with521 | empty =>522 rintro c hs k - A_eq523 have : ∀ i, c i = 0 := by grind524 congr525 ext i j526 rw [A_eq, this, zero_mul, add_zero]527 | insert i s _hi ih =>528 intro c hs k hk A_eq529 have hAi : A i = B i + c i • B k := funext (A_eq i)530 rw [@ih (updateRow B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]531 · exact mt (fun h => show k ∈ insert i s from h ▸ Finset.mem_insert_self _ _) hk532 · intro i' hi'533 rw [Function.update_apply]534 split_ifs with hi'i535 · rfl536 · exact hs i' fun h => hi' ((Finset.mem_insert.mp h).resolve_left hi'i)537 · exact k538 · exact fun h => hk (Finset.mem_insert_of_mem h)539 · intro i' j'540 rw [updateRow_apply, Function.update_apply]541 split_ifs with hi'i542 · simp [hi'i]543 rw [A_eq, updateRow_ne fun h : k = i => hk <| h ▸ Finset.mem_insert_self k s]544545/-- If you add multiples of row `B k` to other rows, the determinant doesn't change. -/546theorem det_eq_of_forall_row_eq_smul_add_const {A B : Matrix n n R} (c : n → R) (k : n)547 (hk : c k = 0) (A_eq : ∀ i j, A i j = B i j + c i * B k j) : det A = det B :=548 det_eq_of_forall_row_eq_smul_add_const_aux c549 (fun i =>550 not_imp_comm.mp fun hi =>551 Finset.mem_erase.mpr552 ⟨mt (fun h : i = k => show c i = 0 from h.symm ▸ hk) hi, Finset.mem_univ i⟩)553 k (Finset.notMem_erase k Finset.univ) A_eq554555theorem det_eq_of_forall_row_eq_smul_add_pred_aux {n : ℕ} (k : Fin (n + 1)) :556 ∀ (c : Fin n → R) (_hc : ∀ i : Fin n, k < i.succ → c i = 0)557 {M N : Matrix (Fin n.succ) (Fin n.succ) R} (_h0 : ∀ j, M 0 j = N 0 j)558 (_hsucc : ∀ (i : Fin n) (j), M i.succ j = N i.succ j + c i * M (Fin.castSucc i) j),559 det M = det N := by560 refine Fin.induction ?_ (fun k ih => ?_) k <;> intro c hc M N h0 hsucc561 · congr562 ext i j563 refine Fin.cases (h0 j) (fun i => ?_) i564 rw [hsucc, hc i (Fin.succ_pos _), zero_mul, add_zero]565 set M' := updateRow M k.succ (N k.succ) with hM'566 have hM : M = updateRow M' k.succ (M' k.succ + c k • M (Fin.castSucc k)) := by567 ext i j568 by_cases hi : i = k.succ569 · simp [hi, hM', hsucc, updateRow_self]570 rw [updateRow_ne hi, hM', updateRow_ne hi]571 have k_ne_succ : (Fin.castSucc k) ≠ k.succ := Fin.castSucc_lt_succ.ne572 have M_k : M (Fin.castSucc k) = M' (Fin.castSucc k) := (updateRow_ne k_ne_succ).symm573 rw [hM, M_k, det_updateRow_add_smul_self M' k_ne_succ.symm, ih (Function.update c k 0)]574 · intro i hi575 rw [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff] at hi576 rw [Function.update_apply]577 split_ifs with hik578 · rfl579 exact hc _ (Fin.succ_lt_succ_iff.mpr (lt_of_le_of_ne hi (Ne.symm hik)))580 · rwa [hM', updateRow_ne (Fin.succ_ne_zero _).symm]581 intro i j582 rw [Function.update_apply]583 split_ifs with hik584 · rw [zero_mul, add_zero, hM', hik, updateRow_self]585 rw [hM', updateRow_ne ((Fin.succ_injective _).ne hik), hsucc]586 by_cases hik2 : k < i587 · simp [hc i (Fin.succ_lt_succ_iff.mpr hik2)]588 rw [updateRow_ne]589 apply ne_of_lt590 rwa [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]591592/-- If you add multiples of previous rows to the next row, the determinant doesn't change. -/593theorem det_eq_of_forall_row_eq_smul_add_pred {n : ℕ} {A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R}594 (c : Fin n → R) (A_zero : ∀ j, A 0 j = B 0 j)595 (A_succ : ∀ (i : Fin n) (j), A i.succ j = B i.succ j + c i * A (Fin.castSucc i) j) :596 det A = det B :=597 det_eq_of_forall_row_eq_smul_add_pred_aux (Fin.last _) c598 (fun _ hi => absurd hi (not_lt_of_ge (Fin.le_last _))) A_zero A_succ599600/-- If you add multiples of previous columns to the next columns, the determinant doesn't change. -/601theorem det_eq_of_forall_col_eq_smul_add_pred {n : ℕ} {A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R}602 (c : Fin n → R) (A_zero : ∀ i, A i 0 = B i 0)603 (A_succ : ∀ (i) (j : Fin n), A i j.succ = B i j.succ + c j * A i (Fin.castSucc j)) :604 det A = det B := by605 rw [← det_transpose A, ← det_transpose B]606 exact det_eq_of_forall_row_eq_smul_add_pred c A_zero fun i j => A_succ j i607608end DetEq609610@[simp]611theorem det_blockDiagonal {o : Type*} [Fintype o] [DecidableEq o] (M : o → Matrix n n R) :612 (blockDiagonal M).det = ∏ k, (M k).det := by613 -- Rewrite the determinants as a sum over permutations.614 simp_rw [det_apply']615 -- The right-hand side is a product of sums, rewrite it as a sum of products.616 rw [Finset.prod_sum]617 simp_rw [Finset.prod_attach_univ, Finset.univ_pi_univ]618 -- We claim that the only permutations contributing to the sum are those that619 -- preserve their second component.620 let preserving_snd : Finset (Equiv.Perm (n × o)) := {σ | ∀ x, (σ x).snd = x.snd}621 have mem_preserving_snd :622 ∀ {σ : Equiv.Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ x, (σ x).snd = x.snd := fun {σ} =>623 Finset.mem_filter.trans ⟨fun h => h.2, fun h => ⟨Finset.mem_univ _, h⟩⟩624 rw [← Finset.sum_subset (Finset.subset_univ preserving_snd) _]625 -- And that these are in bijection with `o → Equiv.Perm m`.626 · refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).symm627 · intro σ _628 rw [mem_preserving_snd]629 rintro ⟨-, x⟩630 simp only [prodCongrLeft_apply]631 · intro σ _ σ' _ eq632 ext x hx k633 have :634 ∀ k x,635 prodCongrLeft (fun k => σ k (Finset.mem_univ _)) (k, x) =636 prodCongrLeft (fun k => σ' k (Finset.mem_univ _)) (k, x) :=637 fun k x => by rw [eq]638 simp only [prodCongrLeft_apply, Prod.mk_inj] at this639 exact (this k x).1640 · intro σ hσ641 rw [mem_preserving_snd] at hσ642 have hσ' x : (σ.symm x).snd = x.snd := by simpa [eq_comm] using hσ (σ.symm x)643 have mk_apply_eq : ∀ k x, ((σ (x, k)).fst, k) = σ (x, k) := by644 intro k x645 ext646 · simp only647 · simp only [hσ]648 have mk_inv_apply_eq : ∀ k x, ((σ.symm (x, k)).fst, k) = σ.symm (x, k) := by grind649 refine ⟨fun k _ => ⟨fun x => (σ (x, k)).fst, fun x => (σ.symm (x, k)).fst, ?_, ?_⟩, ?_, ?_⟩650 · intro x651 simp [mk_apply_eq]652 · intro x653 simp [mk_inv_apply_eq]654 · apply Finset.mem_univ655 · ext ⟨k, x⟩656 · simp only [coe_fn_mk, prodCongrLeft_apply]657 · simp only [prodCongrLeft_apply, hσ]658 · intro σ _659 rw [Finset.prod_mul_distrib, ← Finset.univ_product_univ, Finset.prod_product_right]660 simp only [sign_prodCongrLeft, Units.coe_prod, Int.cast_prod, blockDiagonal_apply_eq,661 prodCongrLeft_apply]662 · intro σ _ hσ663 rw [mem_preserving_snd] at hσ664 obtain ⟨⟨k, x⟩, hkx⟩ := not_forall.mp hσ665 rw [Finset.prod_eq_zero (Finset.mem_univ (k, x)), mul_zero]666 rw [blockDiagonal_apply_ne]667 exact hkx668669/-- The determinant of a 2×2 block matrix with the lower-left block equal to zero is the product of670the determinants of the diagonal blocks. For the generalization to any number of blocks, see671`Matrix.det_of_upperTriangular`. -/672@[simp]673theorem det_fromBlocks_zero₂₁ (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R) :674 (Matrix.fromBlocks A B 0 D).det = A.det * D.det := by675 classical676 simp_rw [det_apply']677 convert!678 Eq.symm <|679 sum_subset (M := R) (subset_univ ((sumCongrHom m n).range : Set (Perm (m ⊕ n))).toFinset) ?_680 · simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]681 refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_682 · intro σ₁₂ _683 simp684 · intro σ₁ _ σ₂ _685 dsimp only686 intro h687 have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=688 DFunLike.congr_fun h689 simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,690 Sum.inr.injEq] at h2691 ext x692 · exact h2.left x693 · exact h2.right x694 · intro σ hσ695 rw [mem_coe, Set.mem_toFinset] at hσ696 obtain ⟨σ₁₂, hσ₁₂⟩ := hσ697 use σ₁₂698 rw [← hσ₁₂]699 simp700 · simp only [forall_prop_of_true, Prod.forall, mem_univ]701 intro σ₁ σ₂702 rw [Fintype.prod_sum_type]703 simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,704 fromBlocks_apply₂₂]705 rw [mul_mul_mul_comm]706 congr707 rw [sign_sumCongr, Units.val_mul, Int.cast_mul]708 · rintro σ - hσn709 have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by710 rw [Set.mem_toFinset] at hσn711 simpa only [Set.MapsTo, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] using712 mt mem_sumCongrHom_range_of_perm_mapsTo_inl hσn713 obtain ⟨a, ha⟩ := not_forall.mp h1714 rcases hx : σ (Sum.inl a) with a2 | b715 · have hn := (not_exists.mp ha) a2716 exact absurd hx.symm hn717 · rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]718 rw [hx, fromBlocks_apply₂₁, zero_apply]719720/-- The determinant of a 2×2 block matrix with the upper-right block equal to zero is the product of721the determinants of the diagonal blocks. For the generalization to any number of blocks, see722`Matrix.det_of_lowerTriangular`. -/723@[simp]724theorem det_fromBlocks_zero₁₂ (A : Matrix m m R) (C : Matrix n m R) (D : Matrix n n R) :725 (Matrix.fromBlocks A 0 C D).det = A.det * D.det := by726 rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose,727 det_transpose]728729/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along column 0. -/730theorem det_succ_column_zero {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) :731 det A = ∑ i : Fin n.succ, (-1) ^ (i : ℕ) * A i 0 * det (A.submatrix i.succAbove Fin.succ) := by732 rw [Matrix.det_apply, Finset.univ_perm_fin_succ, ← Finset.univ_product_univ]733 simp only [Finset.sum_map, Equiv.toEmbedding_apply, Finset.sum_product, Matrix.submatrix]734 refine Finset.sum_congr rfl fun i _ => Fin.cases ?_ (fun i => ?_) i735 · simp only [Fin.prod_univ_succ, Matrix.det_apply, Finset.mul_sum,736 Equiv.Perm.decomposeFin_symm_apply_zero, Fin.val_zero, one_mul,737 Equiv.Perm.decomposeFin.symm_sign, Equiv.swap_self, if_true, id,738 Equiv.Perm.decomposeFin_symm_apply_succ, Fin.succAbove_zero, Equiv.coe_refl, pow_zero,739 mul_smul_comm, of_apply]740 -- `univ_perm_fin_succ` gives a different embedding of `Perm (Fin n)` into741 -- `Perm (Fin n.succ)` than the determinant of the submatrix we want,742 -- permute `A` so that we get the correct one.743 have : (-1 : R) ^ (i : ℕ) = (Perm.sign i.cycleRange) := by simp [Fin.sign_cycleRange]744 rw [Fin.val_succ, pow_succ', this, mul_assoc, mul_assoc, mul_left_comm (ε _),745 ← det_permute, Matrix.det_apply, Finset.mul_sum, Finset.mul_sum]746 -- now we just need to move the corresponding parts to the same place747 refine Finset.sum_congr rfl fun σ _ => ?_748 rw [Equiv.Perm.decomposeFin.symm_sign, if_neg (Fin.succ_ne_zero i)]749 calc750 ((-1 * Perm.sign σ : ℤ) • ∏ i', A (Perm.decomposeFin.symm (Fin.succ i, σ) i') i') =751 (-1 * Perm.sign σ : ℤ) • (A (Fin.succ i) 0 *752 ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by753 simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,754 Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]755 _ = -1 * (A (Fin.succ i) 0 * (Perm.sign σ : ℤ) •756 ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by757 simp [_root_.neg_mul, one_mul, zsmul_eq_mul, neg_smul,758 Fin.succAbove_cycleRange, mul_left_comm]759760/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along row 0. -/761theorem det_succ_row_zero {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) :762 det A = ∑ j : Fin n.succ, (-1) ^ (j : ℕ) * A 0 j * det (A.submatrix Fin.succ j.succAbove) := by763 rw [← det_transpose A, det_succ_column_zero]764 refine Finset.sum_congr rfl fun i _ => ?_765 rw [← det_transpose]766 simp only [transpose_apply, transpose_submatrix, transpose_transpose]767768/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along row `i`. -/769theorem det_succ_row {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin n.succ) :770 det A =771 ∑ j : Fin n.succ, (-1) ^ (i + j : ℕ) * A i j * det (A.submatrix i.succAbove j.succAbove) := by772 simp_rw [pow_add, mul_assoc, ← mul_sum]773 have : det A = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by774 calc775 det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp776 _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]777 rw [this, mul_assoc]778 congr779 rw [← det_permute, det_succ_row_zero]780 refine Finset.sum_congr rfl fun j _ => ?_781 rw [mul_assoc, Matrix.submatrix_apply, submatrix_submatrix, id_comp, Function.comp_def, id]782 simp783784/-- Laplacian expansion of the determinant of an `n+1 × n+1` matrix along column `j`. -/785theorem det_succ_column {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (j : Fin n.succ) :786 det A =787 ∑ i : Fin n.succ, (-1) ^ (i + j : ℕ) * A i j * det (A.submatrix i.succAbove j.succAbove) := by788 rw [← det_transpose, det_succ_row _ j]789 refine Finset.sum_congr rfl fun i _ => ?_790 rw [add_comm, ← det_transpose, transpose_apply, transpose_submatrix, transpose_transpose]791792/-- Determinant of 0x0 matrix -/793@[simp]794theorem det_fin_zero {A : Matrix (Fin 0) (Fin 0) R} : det A = 1 :=795 det_isEmpty796797/-- Determinant of 1x1 matrix -/798theorem det_fin_one (A : Matrix (Fin 1) (Fin 1) R) : det A = A 0 0 :=799 det_unique A800801theorem det_fin_one_of (a : R) : det !![a] = a :=802 det_fin_one _803804/-- Determinant of 2x2 matrix -/805theorem det_fin_two (A : Matrix (Fin 2) (Fin 2) R) : det A = A 0 0 * A 1 1 - A 0 1 * A 1 0 := by806 simp only [det_succ_row_zero, det_unique, Fin.default_eq_zero, submatrix_apply,807 Fin.succ_zero_eq_one, Fin.sum_univ_succ, Fin.val_zero, Fin.zero_succAbove, univ_unique,808 Fin.val_succ, Fin.val_eq_zero, Fin.succ_succAbove_zero, sum_singleton]809 ring810811@[simp]812theorem det_fin_two_of (a b c d : R) : Matrix.det !![a, b; c, d] = a * d - b * c :=813 det_fin_two _814815/-- Determinant of 3x3 matrix -/816theorem det_fin_three (A : Matrix (Fin 3) (Fin 3) R) :817 det A =818 A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1819 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0820 + A 0 2 * A 1 0 * A 2 1 - A 0 2 * A 1 1 * A 2 0 := by821 simp only [det_succ_row_zero, submatrix_apply, Fin.succ_zero_eq_one, submatrix_submatrix,822 det_unique, Fin.default_eq_zero, Function.comp_apply, Fin.succ_one_eq_two, Fin.sum_univ_succ,823 Fin.val_zero, Fin.zero_succAbove, univ_unique, Fin.val_succ, Fin.val_eq_zero,824 Fin.succ_succAbove_zero, sum_singleton, Fin.succ_succAbove_one]825 ring826827end Matrix