Exact source: Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
Pinned GitHub source · Raw UTF-8 source
Back to A common inverse estimate from row Cramer · Back to Cramer’s rule for coordinates of a row
1/-2Copyright (c) 2019 Anne Baanen. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Anne Baanen, Lu-Ming Zhang5-/6module78public import Mathlib.LinearAlgebra.FiniteDimensional.Basic9public import Mathlib.LinearAlgebra.Matrix.Adjugate10public import Mathlib.LinearAlgebra.Matrix.Invertible11public import Mathlib.LinearAlgebra.Matrix.Kronecker12public import Mathlib.LinearAlgebra.Matrix.SemiringInverse13public import Mathlib.LinearAlgebra.Matrix.ToLin14public import Mathlib.LinearAlgebra.Matrix.Trace1516/-!17# Nonsingular inverses1819In this file, we define an inverse for square matrices of invertible determinant.2021For matrices that are not square or not of full rank, there is a more general notion of22pseudoinverses which we do not consider here.2324The definition of inverse used in this file is the adjugate divided by the determinant.25We show that dividing the adjugate by `det A` (if possible), giving a matrix `A⁻¹` (`nonsing_inv`),26will result in a multiplicative inverse to `A`.2728Note that there are at least three different inverses in mathlib:2930* `A⁻¹` (`Inv.inv`): alone, this satisfies no properties, although it is usually used in31 conjunction with `Group` or `GroupWithZero`. On matrices, this is defined to be zero when no32 inverse exists.33* `⅟A` (`invOf`): this is only available in the presence of `[Invertible A]`, which guarantees an34 inverse exists.35* `A⁻¹ʳ`: this is defined on any `MonoidWithZero`, and just like `⁻¹` on matrices, is36 defined to be zero when no inverse exists.3738We start by working with `Invertible`, and show the main results:3940* `Matrix.invertibleOfDetInvertible`41* `Matrix.detInvertibleOfInvertible`42* `Matrix.isUnit_iff_isUnit_det`43* `Matrix.mul_eq_one_comm`4445After this we define `Matrix.inv` and show it matches `⅟A` and `A⁻¹ʳ`.46The rest of the results in the file are then about `A⁻¹`4748## References4950 * https://en.wikipedia.org/wiki/Cramer's_rule#Finding_inverse_matrix5152## Tags5354matrix inverse, cramer, cramer's rule, adjugate55-/5657@[expose] public section585960namespace Matrix6162universe u u' v6364variable {l : Type*} {m : Type u} {n : Type u'} {α : Type v}6566open Matrix Equiv Equiv.Perm Finset67open scoped Ring6869/-! ### Matrices are `Invertible` iff their determinants are -/707172section Invertible7374variable [Fintype n] [DecidableEq n] [CommRing α]75variable (A : Matrix n n α) (B : Matrix n n α)7677/-- If `A.det` has a constructive inverse, produce one for `A`. -/78@[implicit_reducible]79def invertibleOfDetInvertible [Invertible A.det] : Invertible A where80 invOf := ⅟A.det • A.adjugate81 mul_invOf_self := by82 rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]83 invOf_mul_self := by84 rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]8586theorem invOf_eq [Invertible A.det] [Invertible A] : ⅟A = ⅟A.det • A.adjugate := by87 letI := invertibleOfDetInvertible A88 convert! (rfl : ⅟A = _)8990/-- `A.det` is invertible if `A` has a left inverse. -/91@[implicit_reducible]92def detInvertibleOfLeftInverse (h : B * A = 1) : Invertible A.det where93 invOf := B.det94 mul_invOf_self := by rw [mul_comm, ← det_mul, h, det_one]95 invOf_mul_self := by rw [← det_mul, h, det_one]9697/-- `A.det` is invertible if `A` has a right inverse. -/98@[implicit_reducible]99def detInvertibleOfRightInverse (h : A * B = 1) : Invertible A.det where100 invOf := B.det101 mul_invOf_self := by rw [← det_mul, h, det_one]102 invOf_mul_self := by rw [mul_comm, ← det_mul, h, det_one]103104/-- If `A` has a constructive inverse, produce one for `A.det`. -/105@[implicit_reducible]106def detInvertibleOfInvertible [Invertible A] : Invertible A.det :=107 detInvertibleOfLeftInverse A (⅟A) (invOf_mul_self _)108109theorem det_invOf [Invertible A] [Invertible A.det] : (⅟A).det = ⅟A.det := by110 letI := detInvertibleOfInvertible A111 convert! (rfl : _ = ⅟A.det)112113/-- Together `Matrix.detInvertibleOfInvertible` and `Matrix.invertibleOfDetInvertible` form an114equivalence, although both sides of the equiv are subsingleton anyway. -/115@[simps]116def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det where117 toFun := @detInvertibleOfInvertible _ _ _ _ _ A118 invFun := @invertibleOfDetInvertible _ _ _ _ _ A119 left_inv _ := Subsingleton.elim _ _120 right_inv _ := Subsingleton.elim _ _121122/-- Given a proof that `A.det` has a constructive inverse, lift `A` to `(Matrix n n α)ˣ` -/123def unitOfDetInvertible [Invertible A.det] : (Matrix n n α)ˣ :=124 @unitOfInvertible _ _ A (invertibleOfDetInvertible A)125126/-- When lowered to a prop, `Matrix.invertibleEquivDetInvertible` forms an `iff`. -/127theorem isUnit_iff_isUnit_det : IsUnit A ↔ IsUnit A.det := by128 simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivDetInvertible A).nonempty_congr]129130@[simp]131theorem isUnits_det_units (A : (Matrix n n α)ˣ) : IsUnit (A : Matrix n n α).det :=132 isUnit_iff_isUnit_det _ |>.mp A.isUnit133134/-! #### Variants of the statements above with `IsUnit` -/135136137theorem isUnit_det_of_invertible [Invertible A] : IsUnit A.det :=138 @isUnit_of_invertible _ _ _ (detInvertibleOfInvertible A)139140variable {A B}141142theorem isUnit_det_of_left_inverse (h : B * A = 1) : IsUnit A.det :=143 @isUnit_of_invertible _ _ _ (detInvertibleOfLeftInverse _ _ h)144145theorem isUnit_det_of_right_inverse (h : A * B = 1) : IsUnit A.det :=146 @isUnit_of_invertible _ _ _ (detInvertibleOfRightInverse _ _ h)147148theorem det_ne_zero_of_left_inverse [Nontrivial α] (h : B * A = 1) : A.det ≠ 0 :=149 (isUnit_det_of_left_inverse h).ne_zero150151theorem det_ne_zero_of_right_inverse [Nontrivial α] (h : A * B = 1) : A.det ≠ 0 :=152 (isUnit_det_of_right_inverse h).ne_zero153154end Invertible155156section Inv157158variable [Fintype n] [DecidableEq n] [CommRing α]159variable (A : Matrix n n α) (B : Matrix n n α)160161theorem isUnit_det_transpose (h : IsUnit A.det) : IsUnit Aᵀ.det := by162 rw [det_transpose]163 exact h164165/-! ### A noncomputable `Inv` instance -/166167168/-- The inverse of a square matrix, when it is invertible (and zero otherwise). -/169noncomputable instance inv : Inv (Matrix n n α) :=170 ⟨fun A => A.det⁻¹ʳ • A.adjugate⟩171172theorem inv_def (A : Matrix n n α) : A⁻¹ = A.det⁻¹ʳ • A.adjugate :=173 rfl174175theorem nonsing_inv_apply_not_isUnit (h : ¬IsUnit A.det) : A⁻¹ = 0 := by176 rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]177178theorem nonsing_inv_apply (h : IsUnit A.det) : A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate := by179 rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]180181/-- The nonsingular inverse is the same as `invOf` when `A` is invertible. -/182@[simp]183theorem invOf_eq_nonsing_inv [Invertible A] : ⅟A = A⁻¹ := by184 letI := detInvertibleOfInvertible A185 rw [inv_def, Ring.inverse_invertible, invOf_eq]186187/-- Coercing the result of `Units.instInv` is the same as coercing first and applying the188nonsingular inverse. -/189@[simp, norm_cast]190theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α) := by191 letI := A.invertible192 rw [← invOf_eq_nonsing_inv, invOf_units]193194/-- The nonsingular inverse is the same as the general `Ring.inverse`. -/195theorem nonsing_inv_eq_ringInverse : A⁻¹ = A⁻¹ʳ := by196 by_cases h_det : IsUnit A.det197 · cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible198 rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]199 · have h := mt A.isUnit_iff_isUnit_det.mp h_det200 rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]201202theorem transpose_nonsing_inv : A⁻¹ᵀ = Aᵀ⁻¹ := by203 rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]204205theorem conjTranspose_nonsing_inv [StarRing α] : A⁻¹ᴴ = Aᴴ⁻¹ := by206 rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,207 Ring.inverse_star]208209/-- The `nonsing_inv` of `A` is a right inverse. -/210@[simp]211theorem mul_nonsing_inv (h : IsUnit A.det) : A * A⁻¹ = 1 := by212 cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible213 rw [← invOf_eq_nonsing_inv, mul_invOf_self]214215/-- The nonsingular inverse of `A` is a left inverse. -/216@[simp]217theorem nonsing_inv_mul (h : IsUnit A.det) : A⁻¹ * A = 1 := by218 cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible219 rw [← invOf_eq_nonsing_inv, invOf_mul_self]220221instance [Invertible A] : Invertible A⁻¹ := by222 rw [← invOf_eq_nonsing_inv]223 infer_instance224225@[simp]226theorem inv_inv_of_invertible [Invertible A] : A⁻¹⁻¹ = A := by227 simp only [← invOf_eq_nonsing_inv, invOf_invOf]228229@[simp]230theorem mul_nonsing_inv_cancel_right (B : Matrix m n α) (h : IsUnit A.det) : B * A * A⁻¹ = B := by231 simp [Matrix.mul_assoc, mul_nonsing_inv A h]232233@[simp]234theorem mul_nonsing_inv_cancel_left (B : Matrix n m α) (h : IsUnit A.det) : A * (A⁻¹ * B) = B := by235 simp [← Matrix.mul_assoc, mul_nonsing_inv A h]236237@[simp]238theorem nonsing_inv_mul_cancel_right (B : Matrix m n α) (h : IsUnit A.det) : B * A⁻¹ * A = B := by239 simp [Matrix.mul_assoc, nonsing_inv_mul A h]240241@[simp]242theorem nonsing_inv_mul_cancel_left (B : Matrix n m α) (h : IsUnit A.det) : A⁻¹ * (A * B) = B := by243 simp [← Matrix.mul_assoc, nonsing_inv_mul A h]244245@[simp]246theorem mul_inv_of_invertible [Invertible A] : A * A⁻¹ = 1 :=247 mul_nonsing_inv A (isUnit_det_of_invertible A)248249@[simp]250theorem inv_mul_of_invertible [Invertible A] : A⁻¹ * A = 1 :=251 nonsing_inv_mul A (isUnit_det_of_invertible A)252253@[simp]254theorem mul_inv_cancel_right_of_invertible (B : Matrix m n α) [Invertible A] : B * A * A⁻¹ = B :=255 mul_nonsing_inv_cancel_right A B (isUnit_det_of_invertible A)256257@[simp]258theorem mul_inv_cancel_left_of_invertible (B : Matrix n m α) [Invertible A] : A * (A⁻¹ * B) = B :=259 mul_nonsing_inv_cancel_left A B (isUnit_det_of_invertible A)260261@[simp]262theorem inv_mul_cancel_right_of_invertible (B : Matrix m n α) [Invertible A] : B * A⁻¹ * A = B :=263 nonsing_inv_mul_cancel_right A B (isUnit_det_of_invertible A)264265@[simp]266theorem inv_mul_cancel_left_of_invertible (B : Matrix n m α) [Invertible A] : A⁻¹ * (A * B) = B :=267 nonsing_inv_mul_cancel_left A B (isUnit_det_of_invertible A)268269theorem inv_mul_eq_iff_eq_mul_of_invertible (A : Matrix n n α) [Invertible A] (B C : Matrix n m α) :270 A⁻¹ * B = C ↔ B = A * C :=271 ⟨fun h => by rw [← h, mul_inv_cancel_left_of_invertible],272 fun h => by rw [h, inv_mul_cancel_left_of_invertible]⟩273274theorem mul_inv_eq_iff_eq_mul_of_invertible (A : Matrix n n α) [Invertible A] (B C : Matrix m n α) :275 B * A⁻¹ = C ↔ B = C * A :=276 ⟨fun h => by rw [← h, inv_mul_cancel_right_of_invertible],277 fun h => by rw [h, mul_inv_cancel_right_of_invertible]⟩278279lemma inv_mulVec_eq_vec {A : Matrix n n α} [Invertible A]280 {u v : n → α} (hM : u = A.mulVec v) : A⁻¹.mulVec u = v := by281 rw [hM, Matrix.mulVec_mulVec, Matrix.inv_mul_of_invertible, Matrix.one_mulVec]282283lemma mul_right_injective_of_invertible [Invertible A] :284 Function.Injective (fun (x : Matrix n m α) => A * x) :=285 fun _ _ h => by simpa only [inv_mul_cancel_left_of_invertible] using congr_arg (A⁻¹ * ·) h286287lemma mul_left_injective_of_invertible [Invertible A] :288 Function.Injective (fun (x : Matrix m n α) => x * A) :=289 fun a x hax => by simpa only [mul_inv_cancel_right_of_invertible] using congr_arg (· * A⁻¹) hax290291lemma mul_right_inj_of_invertible [Invertible A] {x y : Matrix n m α} : A * x = A * y ↔ x = y :=292 (mul_right_injective_of_invertible A).eq_iff293294lemma mul_left_inj_of_invertible [Invertible A] {x y : Matrix m n α} : x * A = y * A ↔ x = y :=295 (mul_left_injective_of_invertible A).eq_iff296297lemma IsSymm.inv {A : Matrix n n α} (hA : A.IsSymm) : A⁻¹.IsSymm :=298 hA.adjugate.smul _299300end Inv301302section InjectiveMul303variable [Fintype n] [Fintype m] [DecidableEq m] [CommRing α]304305lemma mul_left_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :306 Function.Injective (fun x : Matrix l m α => x * A) := fun _ _ g => by307 simpa only [Matrix.mul_assoc, Matrix.mul_one, h] using congr_arg (· * B) g308309lemma mul_right_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :310 Function.Injective (fun x : Matrix m l α => B * x) :=311 fun _ _ g => by simpa only [← Matrix.mul_assoc, Matrix.one_mul, h] using congr_arg (A * ·) g312313end InjectiveMul314315section vecMul316317section Semiring318319variable {R : Type*} [Semiring R]320321theorem vecMul_surjective_iff_exists_left_inverse322 [DecidableEq n] [Fintype m] [Finite n] {A : Matrix m n R} :323 Function.Surjective A.vecMul ↔ ∃ B : Matrix n m R, B * A = 1 := by324 cases nonempty_fintype n325 refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, by simp [hBA]⟩⟩326 choose rows hrows using (h <| Pi.single · 1)327 refine ⟨Matrix.of rows, Matrix.ext fun i j => ?_⟩328 rw [mul_apply_eq_vecMul, one_eq_pi_single, ← hrows]329 rfl330331theorem mulVec_surjective_iff_exists_right_inverse332 [DecidableEq m] [Finite m] [Fintype n] {A : Matrix m n R} :333 Function.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1 := by334 cases nonempty_fintype m335 refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩336 choose cols hcols using (h <| Pi.single · 1)337 refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩338 rw [one_eq_pi_single, Pi.single_comm, ← hcols j]339 rfl340341end Semiring342343variable [DecidableEq m] {R K : Type*} [CommRing R] [Field K] [Fintype m]344345theorem vecMul_surjective_iff_isUnit {A : Matrix m m R} :346 Function.Surjective A.vecMul ↔ IsUnit A := by347 rw [vecMul_surjective_iff_exists_left_inverse, isUnit_iff_exists_inv']348349theorem mulVec_surjective_iff_isUnit {A : Matrix m m R} :350 Function.Surjective A.mulVec ↔ IsUnit A := by351 rw [mulVec_surjective_iff_exists_right_inverse, isUnit_iff_exists_inv]352353theorem vecMul_injective_iff_isUnit {A : Matrix m m K} :354 Function.Injective A.vecMul ↔ IsUnit A := by355 refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩356 · rw [← vecMul_surjective_iff_isUnit]357 exact LinearMap.surjective_of_injective (f := A.vecMulLinear) h358 exact vecMul_injective_of_isUnit h359360theorem mulVec_injective_iff_isUnit {A : Matrix m m K} :361 Function.Injective A.mulVec ↔ IsUnit A := by362 rw [← isUnit_transpose, ← vecMul_injective_iff_isUnit]363 simp_rw [vecMul_transpose]364365theorem linearIndependent_rows_iff_isUnit {A : Matrix m m K} :366 LinearIndependent K A.row ↔ IsUnit A := by367 rw [← col_transpose, ← mulVec_injective_iff, ← coe_mulVecLin, mulVecLin_transpose,368 ← vecMul_injective_iff_isUnit, coe_vecMulLinear]369370theorem linearIndependent_cols_iff_isUnit {A : Matrix m m K} :371 LinearIndependent K A.col ↔ IsUnit A := by372 rw [← row_transpose, linearIndependent_rows_iff_isUnit, isUnit_transpose]373374theorem vecMul_surjective_of_invertible (A : Matrix m m R) [Invertible A] :375 Function.Surjective A.vecMul :=376 vecMul_surjective_iff_isUnit.2 <| isUnit_of_invertible A377378theorem mulVec_surjective_of_invertible (A : Matrix m m R) [Invertible A] :379 Function.Surjective A.mulVec :=380 mulVec_surjective_iff_isUnit.2 <| isUnit_of_invertible A381382theorem vecMul_injective_of_invertible (A : Matrix m m K) [Invertible A] :383 Function.Injective A.vecMul :=384 vecMul_injective_iff_isUnit.2 <| isUnit_of_invertible A385386theorem mulVec_injective_of_invertible (A : Matrix m m K) [Invertible A] :387 Function.Injective A.mulVec :=388 mulVec_injective_iff_isUnit.2 <| isUnit_of_invertible A389390theorem linearIndependent_rows_of_invertible (A : Matrix m m K) [Invertible A] :391 LinearIndependent K A.row :=392 linearIndependent_rows_iff_isUnit.2 <| isUnit_of_invertible A393394theorem linearIndependent_cols_of_invertible (A : Matrix m m K) [Invertible A] :395 LinearIndependent K A.col :=396 linearIndependent_cols_iff_isUnit.2 <| isUnit_of_invertible A397398end vecMul399400variable [Fintype n] [DecidableEq n] [CommRing α]401variable (A : Matrix n n α) (B : Matrix n n α)402403theorem nonsing_inv_cancel_or_zero : A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0 := by404 by_cases h : IsUnit A.det405 · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩406 · exact Or.inr (nonsing_inv_apply_not_isUnit _ h)407408theorem det_nonsing_inv_mul_det (h : IsUnit A.det) : A⁻¹.det * A.det = 1 := by409 rw [← det_mul, A.nonsing_inv_mul h, det_one]410411@[simp]412theorem det_nonsing_inv : A⁻¹.det = A.det⁻¹ʳ := by413 by_cases h : IsUnit A.det414 · cases h.nonempty_invertible415 letI := invertibleOfDetInvertible A416 rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]417 cases isEmpty_or_nonempty n418 · rw [det_isEmpty, det_isEmpty, Ring.inverse_one]419 · rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]420421theorem isUnit_nonsing_inv_det (h : IsUnit A.det) : IsUnit A⁻¹.det :=422 .of_mul_eq_one _ (A.det_nonsing_inv_mul_det h)423424@[simp]425theorem nonsing_inv_nonsing_inv (h : IsUnit A.det) : A⁻¹⁻¹ = A :=426 calc427 A⁻¹⁻¹ = 1 * A⁻¹⁻¹ := by rw [Matrix.one_mul]428 _ = A * A⁻¹ * A⁻¹⁻¹ := by rw [A.mul_nonsing_inv h]429 _ = A := by430 rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_one]431432theorem isUnit_nonsing_inv_det_iff {A : Matrix n n α} : IsUnit A⁻¹.det ↔ IsUnit A.det := by433 rw [Matrix.det_nonsing_inv, isUnit_ringInverse]434435@[simp]436theorem isUnit_nonsing_inv_iff {A : Matrix n n α} : IsUnit A⁻¹ ↔ IsUnit A := by437 simp_rw [isUnit_iff_isUnit_det, isUnit_nonsing_inv_det_iff]438439-- `IsUnit.invertible` lifts the proposition `IsUnit A` to a constructive inverse of `A`.440/-- A version of `Matrix.invertibleOfDetInvertible` with the inverse defeq to `A⁻¹` that is441therefore noncomputable. -/442@[implicit_reducible]443noncomputable def invertibleOfIsUnitDet (h : IsUnit A.det) : Invertible A :=444 ⟨A⁻¹, nonsing_inv_mul A h, mul_nonsing_inv A h⟩445446/-- A version of `Matrix.unitOfDetInvertible` with the inverse defeq to `A⁻¹` that is therefore447noncomputable. -/448noncomputable def nonsingInvUnit (h : IsUnit A.det) : (Matrix n n α)ˣ :=449 @unitOfInvertible _ _ _ (invertibleOfIsUnitDet A h)450451theorem unitOfDetInvertible_eq_nonsingInvUnit [Invertible A.det] :452 unitOfDetInvertible A = nonsingInvUnit A (isUnit_of_invertible _) := by453 ext454 rfl455456variable {A} {B}457458/-- If matrix A is left invertible, then its inverse equals its left inverse. -/459theorem inv_eq_left_inv (h : B * A = 1) : A⁻¹ = B :=460 letI := invertibleOfLeftInverse _ _ h461 invOf_eq_nonsing_inv A ▸ invOf_eq_left_inv h462463/-- If matrix A is right invertible, then its inverse equals its right inverse. -/464theorem inv_eq_right_inv (h : A * B = 1) : A⁻¹ = B :=465 inv_eq_left_inv (mul_eq_one_comm.2 h)466467section InvEqInv468469variable {C : Matrix n n α}470471/-- The left inverse of matrix A is unique when existing. -/472theorem left_inv_eq_left_inv (h : B * A = 1) (g : C * A = 1) : B = C := by473 rw [← inv_eq_left_inv h, ← inv_eq_left_inv g]474475/-- The right inverse of matrix A is unique when existing. -/476theorem right_inv_eq_right_inv (h : A * B = 1) (g : A * C = 1) : B = C := by477 rw [← inv_eq_right_inv h, ← inv_eq_right_inv g]478479/-- The right inverse of matrix A equals the left inverse of A when they exist. -/480theorem right_inv_eq_left_inv (h : A * B = 1) (g : C * A = 1) : B = C := by481 rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]482483theorem inv_inj (h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) : A = B := by484 refine left_inv_eq_left_inv (mul_nonsing_inv _ h') ?_485 rw [h]486 refine mul_nonsing_inv _ ?_487 rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]488489end InvEqInv490491variable (A)492493set_option backward.isDefEq.respectTransparency false in494@[simp]495theorem inv_zero : (0 : Matrix n n α)⁻¹ = 0 := by496 rcases subsingleton_or_nontrivial α with ht | ht497 · simp [eq_iff_true_of_subsingleton]498 rcases (Fintype.card n).zero_le.eq_or_lt with hc | hc499 · rw [eq_comm, Fintype.card_eq_zero_iff] at hc500 subsingleton501 · have hn : Nonempty n := Fintype.card_pos_iff.mp hc502 refine nonsing_inv_apply_not_isUnit _ ?_503 simp [det]504505noncomputable instance : InvOneClass (Matrix n n α) :=506 { Matrix.one, Matrix.inv with inv_one := inv_eq_left_inv (by simp) }507508theorem inv_smul (k : α) [Invertible k] (h : IsUnit A.det) : (k • A)⁻¹ = ⅟k • A⁻¹ :=509 inv_eq_left_inv (by simp [h, smul_smul])510511theorem inv_smul' (k : αˣ) (h : IsUnit A.det) : (k • A)⁻¹ = k⁻¹ • A⁻¹ :=512 inv_eq_left_inv (by simp [h, smul_smul])513514theorem inv_adjugate (A : Matrix n n α) (h : IsUnit A.det) : (adjugate A)⁻¹ = h.unit⁻¹ • A := by515 refine inv_eq_left_inv ?_516 rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]517518section Diagonal519520attribute [local instance] Invertible.map in521/-- `diagonal v` is invertible if `v` is -/522@[implicit_reducible]523def diagonalInvertible {α} [NonAssocSemiring α] (v : n → α) [Invertible v] :524 Invertible (diagonal v) :=525 inferInstanceAs <| Invertible (diagonalRingHom n α v)526527theorem invOf_diagonal_eq {α} [Semiring α] (v : n → α) [Invertible v] [Invertible (diagonal v)] :528 ⅟(diagonal v) = diagonal (⅟v) := by529 rw [@Invertible.congr _ _ _ _ _ (diagonalInvertible v) rfl]530 rfl531532/-- `v` is invertible if `diagonal v` is -/533@[implicit_reducible]534def invertibleOfDiagonalInvertible (v : n → α) [Invertible (diagonal v)] : Invertible v where535 invOf := diag (⅟(diagonal v))536 invOf_mul_self :=537 funext fun i => by538 letI : Invertible (diagonal v).det := detInvertibleOfInvertible _539 rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]540 dsimp541 rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal]542 exact mul_invOf_self _543 mul_invOf_self :=544 funext fun i => by545 letI : Invertible (diagonal v).det := detInvertibleOfInvertible _546 rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]547 dsimp548 rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]549 exact mul_invOf_self _550551/-- Together `Matrix.diagonalInvertible` and `Matrix.invertibleOfDiagonalInvertible` form an552equivalence, although both sides of the equiv are subsingleton anyway. -/553@[simps]554def diagonalInvertibleEquivInvertible (v : n → α) : Invertible (diagonal v) ≃ Invertible v where555 toFun := @invertibleOfDiagonalInvertible _ _ _ _ _ _556 invFun := @diagonalInvertible _ _ _ _ _ _557 left_inv _ := Subsingleton.elim _ _558 right_inv _ := Subsingleton.elim _ _559560/-- When lowered to a prop, `Matrix.diagonalInvertibleEquivInvertible` forms an `iff`. -/561@[simp]562theorem isUnit_diagonal {v : n → α} : IsUnit (diagonal v) ↔ IsUnit v := by563 simp only [← nonempty_invertible_iff_isUnit,564 (diagonalInvertibleEquivInvertible v).nonempty_congr]565566theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal v⁻¹ʳ := by567 rw [nonsing_inv_eq_ringInverse]568 by_cases h : IsUnit v569 · have := isUnit_diagonal.mpr h570 cases this.nonempty_invertible571 cases h.nonempty_invertible572 rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]573 · have := isUnit_diagonal.not.mpr h574 rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]575576end Diagonal577578/-- The inverse of a 1×1 or 0×0 matrix is always diagonal.579580While we could write this as `of fun _ _ => (A default default)⁻¹ʳ` on the RHS, this is581less useful because:582583* It wouldn't work for 0×0 matrices.584* More things are true about diagonal matrices than constant matrices, and so more lemmas exist.585586`Matrix.diagonal_unique` can be used to reach this form, while `Ring.inverse_eq_inv` can be used587to replace `Ring.inverse` with `⁻¹`.588-/589@[simp]590theorem inv_subsingleton [Subsingleton m] [Fintype m] [DecidableEq m] (A : Matrix m m α) :591 A⁻¹ = diagonal fun i => (A i i)⁻¹ʳ := by592 rw [inv_def, adjugate_subsingleton, smul_one_eq_diagonal]593 congr! with i594 exact det_eq_elem_of_subsingleton _ _595596section Woodbury597598variable [Fintype m] [DecidableEq m]599variable (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)600601/-- The **Woodbury Identity** (`⁻¹` version).602603See `add_mul_mul_inv_eq_sub'` for the binomial inverse theorem. -/604theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)) :605 (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹ := by606 obtain ⟨_⟩ := hA.nonempty_invertible607 obtain ⟨_⟩ := hC.nonempty_invertible608 obtain ⟨iAC⟩ := hAC.nonempty_invertible609 simp only [← invOf_eq_nonsing_inv] at iAC610 letI := invertibleAddMulMul A U C V611 simp only [← invOf_eq_nonsing_inv]612 apply invOf_add_mul_mul613614/-- The **binomial inverse theorem** (variant of the Woodbury identity). -/615theorem add_mul_mul_inv_eq_sub' (hA : IsUnit A) (h : IsUnit (C + C * V * A⁻¹ * U * C)) :616 (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * C * (C + C * V * A⁻¹ * U * C)⁻¹ * C * V * A⁻¹ := by617 obtain ⟨_⟩ := hA.nonempty_invertible618 obtain ⟨ih⟩ := h.nonempty_invertible619 simp only [← invOf_eq_nonsing_inv] at ih620 letI := invertibleAddMulMul' A U C V621 simp only [← invOf_eq_nonsing_inv]622 apply invOf_add_mul_mul'623624end Woodbury625626@[simp]627theorem inv_inv_inv (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ := by628 by_cases h : IsUnit A.det629 · rw [nonsing_inv_nonsing_inv _ h]630 · simp [nonsing_inv_apply_not_isUnit _ h]631632/-- The `Matrix` version of `inv_add_inv'` -/633theorem inv_add_inv {A B : Matrix n n α} (h : IsUnit A ↔ IsUnit B) :634 A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹ := by635 simpa only [nonsing_inv_eq_ringInverse] using Ring.inverse_add_inverse h636637/-- The `Matrix` version of `inv_sub_inv'` -/638theorem inv_sub_inv {A B : Matrix n n α} (h : IsUnit A ↔ IsUnit B) :639 A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹ := by640 simpa only [nonsing_inv_eq_ringInverse] using Ring.inverse_sub_inverse h641642theorem mul_inv_rev (A B : Matrix n n α) : (A * B)⁻¹ = B⁻¹ * A⁻¹ := by643 simp only [inv_def]644 rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,645 Ring.mul_inverse_rev]646647/-- A version of `List.prod_inv_reverse` for `Matrix.inv`. -/648theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.reverse.map Inv.inv).prod649 | [] => by rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]650 | A::Xs => by651 rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons,652 mul_inv_rev, list_prod_inv_reverse Xs]653654/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/655@[simp]656theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :657 A.det • A⁻¹ *ᵥ b = cramer A b := by658 rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul,659 h.mul_val_inv, one_smul]660661/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/662@[simp]663theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :664 A.det • b ᵥ* A⁻¹ = cramer Aᵀ b := by665 rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,666 Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]667668/-! ### Inverses of permutated matrices669670Note that the simp-normal form of `Matrix.reindex` is `Matrix.submatrix`, so we prove most of these671results about only the latter.672-/673674675section Submatrix676677variable [Fintype m]678variable [DecidableEq m]679680/-- `A.submatrix e₁ e₂` is invertible if `A` is -/681@[implicit_reducible]682def submatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] :683 Invertible (A.submatrix e₁ e₂) :=684 invertibleOfRightInverse _ ((⅟A).submatrix e₂ e₁) <| by685 rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]686687/-- `A` is invertible if `A.submatrix e₁ e₂` is -/688@[implicit_reducible]689def invertibleOfSubmatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m)690 [Invertible (A.submatrix e₁ e₂)] : Invertible A :=691 invertibleOfRightInverse _ ((⅟(A.submatrix e₁ e₂)).submatrix e₂.symm e₁.symm) <| by692 have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by simp693 conv in _ * _ =>694 congr695 rw [this]696 rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]697698theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A]699 [Invertible (A.submatrix e₁ e₂)] : ⅟(A.submatrix e₁ e₂) = (⅟A).submatrix e₂ e₁ := by700 rw [@Invertible.congr _ _ _ _ _ (submatrixEquivInvertible A e₁ e₂) rfl]701 rfl702703/-- Together `Matrix.submatrixEquivInvertible` and704`Matrix.invertibleOfSubmatrixEquivInvertible` form an equivalence, although both sides of the705equiv are subsingleton anyway. -/706@[simps]707def submatrixEquivInvertibleEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) :708 Invertible (A.submatrix e₁ e₂) ≃ Invertible A where709 toFun _ := invertibleOfSubmatrixEquivInvertible A e₁ e₂710 invFun _ := submatrixEquivInvertible A e₁ e₂711 left_inv _ := Subsingleton.elim _ _712 right_inv _ := Subsingleton.elim _ _713714/-- When lowered to a prop, `Matrix.invertibleOfSubmatrixEquivInvertible` forms an `iff`. -/715@[simp]716theorem isUnit_submatrix_equiv {A : Matrix m m α} (e₁ e₂ : n ≃ m) :717 IsUnit (A.submatrix e₁ e₂) ↔ IsUnit A := by718 simp only [← nonempty_invertible_iff_isUnit,719 (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr]720721@[simp]722theorem inv_submatrix_equiv (A : Matrix m m α) (e₁ e₂ : n ≃ m) :723 (A.submatrix e₁ e₂)⁻¹ = A⁻¹.submatrix e₂ e₁ := by724 by_cases h : IsUnit A725 · cases h.nonempty_invertible726 letI := submatrixEquivInvertible A e₁ e₂727 rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]728 · have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h729 simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this,730 submatrix_zero, Pi.zero_apply]731732theorem inv_reindex (e₁ e₂ : n ≃ m) (A : Matrix n n α) : (reindex e₁ e₂ A)⁻¹ = reindex e₂ e₁ A⁻¹ :=733 inv_submatrix_equiv A e₁.symm e₂.symm734735end Submatrix736737open scoped Kronecker in738theorem inv_kronecker [Fintype m] [DecidableEq m]739 (A : Matrix m m α) (B : Matrix n n α) : (A ⊗ₖ B)⁻¹ = A⁻¹ ⊗ₖ B⁻¹ := by740 -- handle the special cases where either matrix is not invertible741 by_cases hA : IsUnit A.det742 swap743 · cases isEmpty_or_nonempty n744 · subsingleton745 have hAB : ¬IsUnit (A ⊗ₖ B).det := by746 refine mt (fun hAB => ?_) hA747 rw [det_kronecker] at hAB748 exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_left hAB)749 rw [nonsing_inv_apply_not_isUnit _ hA, zero_kronecker, nonsing_inv_apply_not_isUnit _ hAB]750 by_cases hB : IsUnit B.det; swap751 · cases isEmpty_or_nonempty m752 · subsingleton753 have hAB : ¬IsUnit (A ⊗ₖ B).det := by754 refine mt (fun hAB => ?_) hB755 rw [det_kronecker] at hAB756 exact (isUnit_pow_iff Fintype.card_ne_zero).mp (isUnit_of_mul_isUnit_right hAB)757 rw [nonsing_inv_apply_not_isUnit _ hB, kronecker_zero, nonsing_inv_apply_not_isUnit _ hAB]758 -- otherwise follows trivially from `mul_kronecker_mul`759 · apply inv_eq_right_inv760 rw [← mul_kronecker_mul, ← one_kronecker_one, mul_nonsing_inv _ hA, mul_nonsing_inv _ hB]761762763/-! ### More results about determinants -/764765766section Det767768variable [Fintype m] [DecidableEq m]769770/-- A variant of `Matrix.det_units_conj`. -/771theorem det_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :772 det (M * N * M⁻¹) = det N := by rw [← h.unit_spec, ← coe_units_inv, det_units_conj]773774/-- A variant of `Matrix.det_units_conj'`. -/775theorem det_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :776 det (M⁻¹ * N * M) = det N := by rw [← h.unit_spec, ← coe_units_inv, det_units_conj']777778end Det779780/-! ### More results about traces -/781782783section trace784785variable [Fintype m] [DecidableEq m]786787/-- A variant of `Matrix.trace_units_conj`. -/788theorem trace_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :789 trace (M * N * M⁻¹) = trace N := by rw [← h.unit_spec, ← coe_units_inv, trace_units_conj]790791/-- A variant of `Matrix.trace_units_conj'`. -/792theorem trace_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :793 trace (M⁻¹ * N * M) = trace N := by rw [← h.unit_spec, ← coe_units_inv, trace_units_conj']794795end trace796797end Matrix