From ebd3c064c0b17cb49114119ddce1f028dadf4f63 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 25 Apr 2023 12:02:53 +0200 Subject: [PATCH 1/8] feat: port LinearAlgebra.Matrix.NonsingularInverse From 0f7fe0283ad6fa806dcdd85aeb5a4560e17f2fd1 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 25 Apr 2023 12:02:53 +0200 Subject: [PATCH 2/8] Initial file copy from mathport --- .../Matrix/NonsingularInverse.lean | 750 ++++++++++++++++++ 1 file changed, 750 insertions(+) create mode 100644 Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean new file mode 100644 index 0000000000000..c8e3d986b97a6 --- /dev/null +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -0,0 +1,750 @@ +/- +Copyright (c) 2019 Tim Baanen. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Tim Baanen, Lu-Ming Zhang + +! This file was ported from Lean 3 source module linear_algebra.matrix.nonsingular_inverse +! leanprover-community/mathlib commit a07a7ae98384cd6485d7825e161e528ba78ef3bc +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.LinearAlgebra.Matrix.Adjugate + +/-! +# Nonsingular inverses + +In this file, we define an inverse for square matrices of invertible determinant. + +For matrices that are not square or not of full rank, there is a more general notion of +pseudoinverses which we do not consider here. + +The definition of inverse used in this file is the adjugate divided by the determinant. +We show that dividing the adjugate by `det A` (if possible), giving a matrix `A⁻¹` (`nonsing_inv`), +will result in a multiplicative inverse to `A`. + +Note that there are at least three different inverses in mathlib: + +* `A⁻¹` (`has_inv.inv`): alone, this satisfies no properties, although it is usually used in + conjunction with `group` or `group_with_zero`. On matrices, this is defined to be zero when no + inverse exists. +* `⅟A` (`inv_of`): this is only available in the presence of `[invertible A]`, which guarantees an + inverse exists. +* `ring.inverse A`: this is defined on any `monoid_with_zero`, and just like `⁻¹` on matrices, is + defined to be zero when no inverse exists. + +We start by working with `invertible`, and show the main results: + +* `matrix.invertible_of_det_invertible` +* `matrix.det_invertible_of_invertible` +* `matrix.is_unit_iff_is_unit_det` +* `matrix.mul_eq_one_comm` + +After this we define `matrix.has_inv` and show it matches `⅟A` and `ring.inverse A`. +The rest of the results in the file are then about `A⁻¹` + +## References + + * https://en.wikipedia.org/wiki/Cramer's_rule#Finding_inverse_matrix + +## Tags + +matrix inverse, cramer, cramer's rule, adjugate +-/ + + +namespace Matrix + +universe u u' v + +variable {l : Type _} {m : Type u} {n : Type u'} {α : Type v} + +open Matrix BigOperators + +open Equiv Equiv.Perm Finset + +/-! ### Matrices are `invertible` iff their determinants are -/ + + +section Invertible + +variable [Fintype n] [DecidableEq n] [CommRing α] + +/-- A copy of `inv_of_mul_self` using `⬝` not `*`. -/ +protected theorem invOf_mul_self (A : Matrix n n α) [Invertible A] : ⅟ A ⬝ A = 1 := + invOf_mul_self A +#align matrix.inv_of_mul_self Matrix.invOf_mul_self + +/-- A copy of `mul_inv_of_self` using `⬝` not `*`. -/ +protected theorem mul_invOf_self (A : Matrix n n α) [Invertible A] : A ⬝ ⅟ A = 1 := + mul_invOf_self A +#align matrix.mul_inv_of_self Matrix.mul_invOf_self + +/-- A copy of `inv_of_mul_self_assoc` using `⬝` not `*`. -/ +protected theorem invOf_mul_self_assoc (A : Matrix n n α) (B : Matrix n m α) [Invertible A] : + ⅟ A ⬝ (A ⬝ B) = B := by rw [← Matrix.mul_assoc, Matrix.invOf_mul_self, Matrix.one_mul] +#align matrix.inv_of_mul_self_assoc Matrix.invOf_mul_self_assoc + +/-- A copy of `mul_inv_of_self_assoc` using `⬝` not `*`. -/ +protected theorem mul_invOf_self_assoc (A : Matrix n n α) (B : Matrix n m α) [Invertible A] : + A ⬝ (⅟ A ⬝ B) = B := by rw [← Matrix.mul_assoc, Matrix.mul_invOf_self, Matrix.one_mul] +#align matrix.mul_inv_of_self_assoc Matrix.mul_invOf_self_assoc + +/-- A copy of `mul_inv_of_mul_self_cancel` using `⬝` not `*`. -/ +protected theorem mul_invOf_mul_self_cancel (A : Matrix m n α) (B : Matrix n n α) [Invertible B] : + A ⬝ ⅟ B ⬝ B = A := by rw [Matrix.mul_assoc, Matrix.invOf_mul_self, Matrix.mul_one] +#align matrix.mul_inv_of_mul_self_cancel Matrix.mul_invOf_mul_self_cancel + +/-- A copy of `mul_mul_inv_of_self_cancel` using `⬝` not `*`. -/ +protected theorem mul_mul_invOf_self_cancel (A : Matrix m n α) (B : Matrix n n α) [Invertible B] : + A ⬝ B ⬝ ⅟ B = A := by rw [Matrix.mul_assoc, Matrix.mul_invOf_self, Matrix.mul_one] +#align matrix.mul_mul_inv_of_self_cancel Matrix.mul_mul_invOf_self_cancel + +variable (A : Matrix n n α) (B : Matrix n n α) + +/-- If `A.det` has a constructive inverse, produce one for `A`. -/ +def invertibleOfDetInvertible [Invertible A.det] : Invertible A + where + invOf := ⅟ A.det • A.adjugate + mul_invOf_self := by + rw [mul_smul_comm, Matrix.mul_eq_mul, mul_adjugate, smul_smul, invOf_mul_self, one_smul] + invOf_mul_self := by + rw [smul_mul_assoc, Matrix.mul_eq_mul, adjugate_mul, smul_smul, invOf_mul_self, one_smul] +#align matrix.invertible_of_det_invertible Matrix.invertibleOfDetInvertible + +theorem invOf_eq [Invertible A.det] [Invertible A] : ⅟ A = ⅟ A.det • A.adjugate := + by + letI := invertible_of_det_invertible A + convert(rfl : ⅟ A = _) +#align matrix.inv_of_eq Matrix.invOf_eq + +/-- `A.det` is invertible if `A` has a left inverse. -/ +def detInvertibleOfLeftInverse (h : B ⬝ A = 1) : Invertible A.det + where + invOf := B.det + mul_invOf_self := by rw [mul_comm, ← det_mul, h, det_one] + invOf_mul_self := by rw [← det_mul, h, det_one] +#align matrix.det_invertible_of_left_inverse Matrix.detInvertibleOfLeftInverse + +/-- `A.det` is invertible if `A` has a right inverse. -/ +def detInvertibleOfRightInverse (h : A ⬝ B = 1) : Invertible A.det + where + invOf := B.det + mul_invOf_self := by rw [← det_mul, h, det_one] + invOf_mul_self := by rw [mul_comm, ← det_mul, h, det_one] +#align matrix.det_invertible_of_right_inverse Matrix.detInvertibleOfRightInverse + +/-- If `A` has a constructive inverse, produce one for `A.det`. -/ +def detInvertibleOfInvertible [Invertible A] : Invertible A.det := + detInvertibleOfLeftInverse A (⅟ A) (invOf_mul_self _) +#align matrix.det_invertible_of_invertible Matrix.detInvertibleOfInvertible + +theorem det_invOf [Invertible A] [Invertible A.det] : (⅟ A).det = ⅟ A.det := + by + letI := det_invertible_of_invertible A + convert(rfl : _ = ⅟ A.det) +#align matrix.det_inv_of Matrix.det_invOf + +/-- Together `matrix.det_invertible_of_invertible` and `matrix.invertible_of_det_invertible` form an +equivalence, although both sides of the equiv are subsingleton anyway. -/ +@[simps] +def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det + where + toFun := @detInvertibleOfInvertible _ _ _ _ _ A + invFun := @invertibleOfDetInvertible _ _ _ _ _ A + left_inv _ := Subsingleton.elim _ _ + right_inv _ := Subsingleton.elim _ _ +#align matrix.invertible_equiv_det_invertible Matrix.invertibleEquivDetInvertible + +variable {A B} + +theorem mul_eq_one_comm : A ⬝ B = 1 ↔ B ⬝ A = 1 := + suffices ∀ A B, A ⬝ B = 1 → B ⬝ A = 1 from ⟨this A B, this B A⟩ + fun A B h => by + letI : Invertible B.det := det_invertible_of_left_inverse _ _ h + letI : Invertible B := invertible_of_det_invertible B + calc + B ⬝ A = B ⬝ A ⬝ (B ⬝ ⅟ B) := by rw [Matrix.mul_invOf_self, Matrix.mul_one] + _ = B ⬝ (A ⬝ B ⬝ ⅟ B) := by simp only [Matrix.mul_assoc] + _ = B ⬝ ⅟ B := by rw [h, Matrix.one_mul] + _ = 1 := Matrix.mul_invOf_self B + +#align matrix.mul_eq_one_comm Matrix.mul_eq_one_comm + +variable (A B) + +/-- We can construct an instance of invertible A if A has a left inverse. -/ +def invertibleOfLeftInverse (h : B ⬝ A = 1) : Invertible A := + ⟨B, h, mul_eq_one_comm.mp h⟩ +#align matrix.invertible_of_left_inverse Matrix.invertibleOfLeftInverse + +/-- We can construct an instance of invertible A if A has a right inverse. -/ +def invertibleOfRightInverse (h : A ⬝ B = 1) : Invertible A := + ⟨B, mul_eq_one_comm.mp h, h⟩ +#align matrix.invertible_of_right_inverse Matrix.invertibleOfRightInverse + +/-- The transpose of an invertible matrix is invertible. -/ +instance invertibleTranspose [Invertible A] : Invertible Aᵀ := + haveI : Invertible Aᵀ.det := by simpa using det_invertible_of_invertible A + invertible_of_det_invertible Aᵀ +#align matrix.invertible_transpose Matrix.invertibleTranspose + +/-- A matrix is invertible if the transpose is invertible. -/ +def invertibleOfInvertibleTranspose [Invertible Aᵀ] : Invertible A := + by + rw [← transpose_transpose A] + infer_instance +#align matrix.invertible__of_invertible_transpose Matrix.invertibleOfInvertibleTranspose + +/-- A matrix is invertible if the conjugate transpose is invertible. -/ +def invertibleOfInvertibleConjTranspose [StarRing α] [Invertible Aᴴ] : Invertible A := + by + rw [← conj_transpose_conj_transpose A] + infer_instance +#align matrix.invertible_of_invertible_conj_transpose Matrix.invertibleOfInvertibleConjTranspose + +/-- Given a proof that `A.det` has a constructive inverse, lift `A` to `(matrix n n α)ˣ`-/ +def unitOfDetInvertible [Invertible A.det] : (Matrix n n α)ˣ := + @unitOfInvertible _ _ A (invertibleOfDetInvertible A) +#align matrix.unit_of_det_invertible Matrix.unitOfDetInvertible + +/-- When lowered to a prop, `matrix.invertible_equiv_det_invertible` forms an `iff`. -/ +theorem isUnit_iff_isUnit_det : IsUnit A ↔ IsUnit A.det := by + simp only [← nonempty_invertible_iff_isUnit, (invertible_equiv_det_invertible A).nonempty_congr] +#align matrix.is_unit_iff_is_unit_det Matrix.isUnit_iff_isUnit_det + +/-! #### Variants of the statements above with `is_unit`-/ + + +theorem isUnit_det_of_invertible [Invertible A] : IsUnit A.det := + @isUnit_of_invertible _ _ _ (detInvertibleOfInvertible A) +#align matrix.is_unit_det_of_invertible Matrix.isUnit_det_of_invertible + +variable {A B} + +theorem isUnit_of_left_inverse (h : B ⬝ A = 1) : IsUnit A := + ⟨⟨A, B, mul_eq_one_comm.mp h, h⟩, rfl⟩ +#align matrix.is_unit_of_left_inverse Matrix.isUnit_of_left_inverse + +theorem isUnit_of_right_inverse (h : A ⬝ B = 1) : IsUnit A := + ⟨⟨A, B, h, mul_eq_one_comm.mp h⟩, rfl⟩ +#align matrix.is_unit_of_right_inverse Matrix.isUnit_of_right_inverse + +theorem isUnit_det_of_left_inverse (h : B ⬝ A = 1) : IsUnit A.det := + @isUnit_of_invertible _ _ _ (detInvertibleOfLeftInverse _ _ h) +#align matrix.is_unit_det_of_left_inverse Matrix.isUnit_det_of_left_inverse + +theorem isUnit_det_of_right_inverse (h : A ⬝ B = 1) : IsUnit A.det := + @isUnit_of_invertible _ _ _ (detInvertibleOfRightInverse _ _ h) +#align matrix.is_unit_det_of_right_inverse Matrix.isUnit_det_of_right_inverse + +theorem det_ne_zero_of_left_inverse [Nontrivial α] (h : B ⬝ A = 1) : A.det ≠ 0 := + (isUnit_det_of_left_inverse h).NeZero +#align matrix.det_ne_zero_of_left_inverse Matrix.det_ne_zero_of_left_inverse + +theorem det_ne_zero_of_right_inverse [Nontrivial α] (h : A ⬝ B = 1) : A.det ≠ 0 := + (isUnit_det_of_right_inverse h).NeZero +#align matrix.det_ne_zero_of_right_inverse Matrix.det_ne_zero_of_right_inverse + +end Invertible + +variable [Fintype n] [DecidableEq n] [CommRing α] + +variable (A : Matrix n n α) (B : Matrix n n α) + +theorem isUnit_det_transpose (h : IsUnit A.det) : IsUnit Aᵀ.det := + by + rw [det_transpose] + exact h +#align matrix.is_unit_det_transpose Matrix.isUnit_det_transpose + +/-! ### A noncomputable `has_inv` instance -/ + + +/-- The inverse of a square matrix, when it is invertible (and zero otherwise).-/ +noncomputable instance : Inv (Matrix n n α) := + ⟨fun A => Ring.inverse A.det • A.adjugate⟩ + +theorem inv_def (A : Matrix n n α) : A⁻¹ = Ring.inverse A.det • A.adjugate := + rfl +#align matrix.inv_def Matrix.inv_def + +theorem nonsing_inv_apply_not_isUnit (h : ¬IsUnit A.det) : A⁻¹ = 0 := by + rw [inv_def, Ring.inverse_non_unit _ h, zero_smul] +#align matrix.nonsing_inv_apply_not_is_unit Matrix.nonsing_inv_apply_not_isUnit + +theorem nonsing_inv_apply (h : IsUnit A.det) : A⁻¹ = (↑h.Unit⁻¹ : α) • A.adjugate := by + rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec] +#align matrix.nonsing_inv_apply Matrix.nonsing_inv_apply + +/-- The nonsingular inverse is the same as `inv_of` when `A` is invertible. -/ +@[simp] +theorem invOf_eq_nonsing_inv [Invertible A] : ⅟ A = A⁻¹ := + by + letI := det_invertible_of_invertible A + rw [inv_def, Ring.inverse_invertible, inv_of_eq] +#align matrix.inv_of_eq_nonsing_inv Matrix.invOf_eq_nonsing_inv + +/-- Coercing the result of `units.has_inv` is the same as coercing first and applying the +nonsingular inverse. -/ +@[simp, norm_cast] +theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α) := + by + letI := A.invertible + rw [← inv_of_eq_nonsing_inv, invOf_units] +#align matrix.coe_units_inv Matrix.coe_units_inv + +/-- The nonsingular inverse is the same as the general `ring.inverse`. -/ +theorem nonsing_inv_eq_ring_inverse : A⁻¹ = Ring.inverse A := + by + by_cases h_det : IsUnit A.det + · cases (A.is_unit_iff_is_unit_det.mpr h_det).nonempty_invertible + rw [← inv_of_eq_nonsing_inv, Ring.inverse_invertible] + · have h := mt A.is_unit_iff_is_unit_det.mp h_det + rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_is_unit A h_det] +#align matrix.nonsing_inv_eq_ring_inverse Matrix.nonsing_inv_eq_ring_inverse + +theorem transpose_nonsing_inv : A⁻¹ᵀ = Aᵀ⁻¹ := by + rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose] +#align matrix.transpose_nonsing_inv Matrix.transpose_nonsing_inv + +theorem conjTranspose_nonsing_inv [StarRing α] : A⁻¹ᴴ = Aᴴ⁻¹ := by + rw [inv_def, inv_def, conj_transpose_smul, det_conj_transpose, adjugate_conj_transpose, + Ring.inverse_star] +#align matrix.conj_transpose_nonsing_inv Matrix.conjTranspose_nonsing_inv + +/-- The `nonsing_inv` of `A` is a right inverse. -/ +@[simp] +theorem mul_nonsing_inv (h : IsUnit A.det) : A ⬝ A⁻¹ = 1 := + by + cases (A.is_unit_iff_is_unit_det.mpr h).nonempty_invertible + rw [← inv_of_eq_nonsing_inv, Matrix.mul_invOf_self] +#align matrix.mul_nonsing_inv Matrix.mul_nonsing_inv + +/-- The `nonsing_inv` of `A` is a left inverse. -/ +@[simp] +theorem nonsing_inv_mul (h : IsUnit A.det) : A⁻¹ ⬝ A = 1 := + by + cases (A.is_unit_iff_is_unit_det.mpr h).nonempty_invertible + rw [← inv_of_eq_nonsing_inv, Matrix.invOf_mul_self] +#align matrix.nonsing_inv_mul Matrix.nonsing_inv_mul + +instance [Invertible A] : Invertible A⁻¹ := + by + rw [← inv_of_eq_nonsing_inv] + infer_instance + +@[simp] +theorem inv_inv_of_invertible [Invertible A] : A⁻¹⁻¹ = A := by + simp only [← inv_of_eq_nonsing_inv, invOf_invOf] +#align matrix.inv_inv_of_invertible Matrix.inv_inv_of_invertible + +@[simp] +theorem mul_nonsing_inv_cancel_right (B : Matrix m n α) (h : IsUnit A.det) : B ⬝ A ⬝ A⁻¹ = B := by + simp [Matrix.mul_assoc, mul_nonsing_inv A h] +#align matrix.mul_nonsing_inv_cancel_right Matrix.mul_nonsing_inv_cancel_right + +@[simp] +theorem mul_nonsing_inv_cancel_left (B : Matrix n m α) (h : IsUnit A.det) : A ⬝ (A⁻¹ ⬝ B) = B := by + simp [← Matrix.mul_assoc, mul_nonsing_inv A h] +#align matrix.mul_nonsing_inv_cancel_left Matrix.mul_nonsing_inv_cancel_left + +@[simp] +theorem nonsing_inv_mul_cancel_right (B : Matrix m n α) (h : IsUnit A.det) : B ⬝ A⁻¹ ⬝ A = B := by + simp [Matrix.mul_assoc, nonsing_inv_mul A h] +#align matrix.nonsing_inv_mul_cancel_right Matrix.nonsing_inv_mul_cancel_right + +@[simp] +theorem nonsing_inv_mul_cancel_left (B : Matrix n m α) (h : IsUnit A.det) : A⁻¹ ⬝ (A ⬝ B) = B := by + simp [← Matrix.mul_assoc, nonsing_inv_mul A h] +#align matrix.nonsing_inv_mul_cancel_left Matrix.nonsing_inv_mul_cancel_left + +@[simp] +theorem mul_inv_of_invertible [Invertible A] : A ⬝ A⁻¹ = 1 := + mul_nonsing_inv A (isUnit_det_of_invertible A) +#align matrix.mul_inv_of_invertible Matrix.mul_inv_of_invertible + +@[simp] +theorem inv_mul_of_invertible [Invertible A] : A⁻¹ ⬝ A = 1 := + nonsing_inv_mul A (isUnit_det_of_invertible A) +#align matrix.inv_mul_of_invertible Matrix.inv_mul_of_invertible + +@[simp] +theorem mul_inv_cancel_right_of_invertible (B : Matrix m n α) [Invertible A] : B ⬝ A ⬝ A⁻¹ = B := + mul_nonsing_inv_cancel_right A B (isUnit_det_of_invertible A) +#align matrix.mul_inv_cancel_right_of_invertible Matrix.mul_inv_cancel_right_of_invertible + +@[simp] +theorem mul_inv_cancel_left_of_invertible (B : Matrix n m α) [Invertible A] : A ⬝ (A⁻¹ ⬝ B) = B := + mul_nonsing_inv_cancel_left A B (isUnit_det_of_invertible A) +#align matrix.mul_inv_cancel_left_of_invertible Matrix.mul_inv_cancel_left_of_invertible + +@[simp] +theorem inv_mul_cancel_right_of_invertible (B : Matrix m n α) [Invertible A] : B ⬝ A⁻¹ ⬝ A = B := + nonsing_inv_mul_cancel_right A B (isUnit_det_of_invertible A) +#align matrix.inv_mul_cancel_right_of_invertible Matrix.inv_mul_cancel_right_of_invertible + +@[simp] +theorem inv_mul_cancel_left_of_invertible (B : Matrix n m α) [Invertible A] : A⁻¹ ⬝ (A ⬝ B) = B := + nonsing_inv_mul_cancel_left A B (isUnit_det_of_invertible A) +#align matrix.inv_mul_cancel_left_of_invertible Matrix.inv_mul_cancel_left_of_invertible + +theorem inv_mul_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] : + A⁻¹ ⬝ B = C ↔ B = A ⬝ C := + ⟨fun h => by rw [← h, mul_inv_cancel_left_of_invertible], fun h => by + rw [h, inv_mul_cancel_left_of_invertible]⟩ +#align matrix.inv_mul_eq_iff_eq_mul_of_invertible Matrix.inv_mul_eq_iff_eq_mul_of_invertible + +theorem mul_inv_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] : + B ⬝ A⁻¹ = C ↔ B = C ⬝ A := + ⟨fun h => by rw [← h, inv_mul_cancel_right_of_invertible], fun h => by + rw [h, mul_inv_cancel_right_of_invertible]⟩ +#align matrix.mul_inv_eq_iff_eq_mul_of_invertible Matrix.mul_inv_eq_iff_eq_mul_of_invertible + +theorem nonsing_inv_cancel_or_zero : A⁻¹ ⬝ A = 1 ∧ A ⬝ A⁻¹ = 1 ∨ A⁻¹ = 0 := + by + by_cases h : IsUnit A.det + · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩ + · exact Or.inr (nonsing_inv_apply_not_is_unit _ h) +#align matrix.nonsing_inv_cancel_or_zero Matrix.nonsing_inv_cancel_or_zero + +theorem det_nonsing_inv_mul_det (h : IsUnit A.det) : A⁻¹.det * A.det = 1 := by + rw [← det_mul, A.nonsing_inv_mul h, det_one] +#align matrix.det_nonsing_inv_mul_det Matrix.det_nonsing_inv_mul_det + +@[simp] +theorem det_nonsing_inv : A⁻¹.det = Ring.inverse A.det := + by + by_cases h : IsUnit A.det + · cases h.nonempty_invertible + letI := invertible_of_det_invertible A + rw [Ring.inverse_invertible, ← inv_of_eq_nonsing_inv, det_inv_of] + cases isEmpty_or_nonempty n + · rw [det_is_empty, det_is_empty, Ring.inverse_one] + · rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_is_unit _ h, det_zero ‹_›] +#align matrix.det_nonsing_inv Matrix.det_nonsing_inv + +theorem isUnit_nonsing_inv_det (h : IsUnit A.det) : IsUnit A⁻¹.det := + isUnit_of_mul_eq_one _ _ (A.det_nonsing_inv_mul_det h) +#align matrix.is_unit_nonsing_inv_det Matrix.isUnit_nonsing_inv_det + +@[simp] +theorem nonsing_inv_nonsing_inv (h : IsUnit A.det) : A⁻¹⁻¹ = A := + calc + A⁻¹⁻¹ = 1 ⬝ A⁻¹⁻¹ := by rw [Matrix.one_mul] + _ = A ⬝ A⁻¹ ⬝ A⁻¹⁻¹ := by rw [A.mul_nonsing_inv h] + _ = A := by + rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.is_unit_nonsing_inv_det h), Matrix.mul_one] + +#align matrix.nonsing_inv_nonsing_inv Matrix.nonsing_inv_nonsing_inv + +theorem isUnit_nonsing_inv_det_iff {A : Matrix n n α} : IsUnit A⁻¹.det ↔ IsUnit A.det := by + rw [Matrix.det_nonsing_inv, isUnit_ring_inverse] +#align matrix.is_unit_nonsing_inv_det_iff Matrix.isUnit_nonsing_inv_det_iff + +-- `is_unit.invertible` lifts the proposition `is_unit A` to a constructive inverse of `A`. +/-- A version of `matrix.invertible_of_det_invertible` with the inverse defeq to `A⁻¹` that is +therefore noncomputable. -/ +noncomputable def invertibleOfIsUnitDet (h : IsUnit A.det) : Invertible A := + ⟨A⁻¹, nonsing_inv_mul A h, mul_nonsing_inv A h⟩ +#align matrix.invertible_of_is_unit_det Matrix.invertibleOfIsUnitDet + +/-- A version of `matrix.units_of_det_invertible` with the inverse defeq to `A⁻¹` that is therefore +noncomputable. -/ +noncomputable def nonsingInvUnit (h : IsUnit A.det) : (Matrix n n α)ˣ := + @unitOfInvertible _ _ _ (invertibleOfIsUnitDet A h) +#align matrix.nonsing_inv_unit Matrix.nonsingInvUnit + +theorem unitOfDetInvertible_eq_nonsingInvUnit [Invertible A.det] : + unitOfDetInvertible A = nonsingInvUnit A (isUnit_of_invertible _) := + by + ext + rfl +#align matrix.unit_of_det_invertible_eq_nonsing_inv_unit Matrix.unitOfDetInvertible_eq_nonsingInvUnit + +variable {A} {B} + +/-- If matrix A is left invertible, then its inverse equals its left inverse. -/ +theorem inv_eq_left_inv (h : B ⬝ A = 1) : A⁻¹ = B := + letI := invertible_of_left_inverse _ _ h + inv_of_eq_nonsing_inv A ▸ invOf_eq_left_inv h +#align matrix.inv_eq_left_inv Matrix.inv_eq_left_inv + +/-- If matrix A is right invertible, then its inverse equals its right inverse. -/ +theorem inv_eq_right_inv (h : A ⬝ B = 1) : A⁻¹ = B := + inv_eq_left_inv (mul_eq_one_comm.2 h) +#align matrix.inv_eq_right_inv Matrix.inv_eq_right_inv + +section InvEqInv + +variable {C : Matrix n n α} + +/-- The left inverse of matrix A is unique when existing. -/ +theorem left_inv_eq_left_inv (h : B ⬝ A = 1) (g : C ⬝ A = 1) : B = C := by + rw [← inv_eq_left_inv h, ← inv_eq_left_inv g] +#align matrix.left_inv_eq_left_inv Matrix.left_inv_eq_left_inv + +/-- The right inverse of matrix A is unique when existing. -/ +theorem right_inv_eq_right_inv (h : A ⬝ B = 1) (g : A ⬝ C = 1) : B = C := by + rw [← inv_eq_right_inv h, ← inv_eq_right_inv g] +#align matrix.right_inv_eq_right_inv Matrix.right_inv_eq_right_inv + +/-- The right inverse of matrix A equals the left inverse of A when they exist. -/ +theorem right_inv_eq_left_inv (h : A ⬝ B = 1) (g : C ⬝ A = 1) : B = C := by + rw [← inv_eq_right_inv h, ← inv_eq_left_inv g] +#align matrix.right_inv_eq_left_inv Matrix.right_inv_eq_left_inv + +theorem inv_inj (h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) : A = B := + by + refine' left_inv_eq_left_inv (mul_nonsing_inv _ h') _ + rw [h] + refine' mul_nonsing_inv _ _ + rwa [← is_unit_nonsing_inv_det_iff, ← h, is_unit_nonsing_inv_det_iff] +#align matrix.inv_inj Matrix.inv_inj + +end InvEqInv + +variable (A) + +@[simp] +theorem inv_zero : (0 : Matrix n n α)⁻¹ = 0 := + by + cases' subsingleton_or_nontrivial α with ht ht + · simp + cases' (Fintype.card n).zero_le.eq_or_lt with hc hc + · rw [eq_comm, Fintype.card_eq_zero_iff] at hc + haveI := hc + ext i + exact (IsEmpty.false i).elim + · have hn : Nonempty n := fintype.card_pos_iff.mp hc + refine' nonsing_inv_apply_not_is_unit _ _ + simp [hn] +#align matrix.inv_zero Matrix.inv_zero + +noncomputable instance : InvOneClass (Matrix n n α) := + { Matrix.hasOne, Matrix.hasInv with inv_one := inv_eq_left_inv (by simp) } + +theorem inv_smul (k : α) [Invertible k] (h : IsUnit A.det) : (k • A)⁻¹ = ⅟ k • A⁻¹ := + inv_eq_left_inv (by simp [h, smul_smul]) +#align matrix.inv_smul Matrix.inv_smul + +theorem inv_smul' (k : αˣ) (h : IsUnit A.det) : (k • A)⁻¹ = k⁻¹ • A⁻¹ := + inv_eq_left_inv (by simp [h, smul_smul]) +#align matrix.inv_smul' Matrix.inv_smul' + +theorem inv_adjugate (A : Matrix n n α) (h : IsUnit A.det) : (adjugate A)⁻¹ = h.Unit⁻¹ • A := + by + refine' inv_eq_left_inv _ + rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.coe_inv_mul, one_smul] +#align matrix.inv_adjugate Matrix.inv_adjugate + +section Diagonal + +/-- `diagonal v` is invertible if `v` is -/ +def diagonalInvertible {α} [NonAssocSemiring α] (v : n → α) [Invertible v] : + Invertible (diagonal v) := + Invertible.map (diagonalRingHom n α) v +#align matrix.diagonal_invertible Matrix.diagonalInvertible + +theorem invOf_diagonal_eq {α} [Semiring α] (v : n → α) [Invertible v] [Invertible (diagonal v)] : + ⅟ (diagonal v) = diagonal (⅟ v) := + by + letI := diagonal_invertible v + haveI := Invertible.subsingleton (diagonal v) + convert(rfl : ⅟ (diagonal v) = _) +#align matrix.inv_of_diagonal_eq Matrix.invOf_diagonal_eq + +/-- `v` is invertible if `diagonal v` is -/ +def invertibleOfDiagonalInvertible (v : n → α) [Invertible (diagonal v)] : Invertible v + where + invOf := diag (⅟ (diagonal v)) + invOf_mul_self := + funext fun i => + by + letI : Invertible (diagonal v).det := det_invertible_of_invertible _ + rw [inv_of_eq, diag_smul, adjugate_diagonal, diag_diagonal] + dsimp + rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal] + exact mul_invOf_self _ + mul_invOf_self := + funext fun i => + by + letI : Invertible (diagonal v).det := det_invertible_of_invertible _ + rw [inv_of_eq, diag_smul, adjugate_diagonal, diag_diagonal] + dsimp + rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal] + exact mul_invOf_self _ +#align matrix.invertible_of_diagonal_invertible Matrix.invertibleOfDiagonalInvertible + +/-- Together `matrix.diagonal_invertible` and `matrix.invertible_of_diagonal_invertible` form an +equivalence, although both sides of the equiv are subsingleton anyway. -/ +@[simps] +def diagonalInvertibleEquivInvertible (v : n → α) : Invertible (diagonal v) ≃ Invertible v + where + toFun := @invertibleOfDiagonalInvertible _ _ _ _ _ _ + invFun := @diagonalInvertible _ _ _ _ _ _ + left_inv _ := Subsingleton.elim _ _ + right_inv _ := Subsingleton.elim _ _ +#align matrix.diagonal_invertible_equiv_invertible Matrix.diagonalInvertibleEquivInvertible + +/-- When lowered to a prop, `matrix.diagonal_invertible_equiv_invertible` forms an `iff`. -/ +@[simp] +theorem isUnit_diagonal {v : n → α} : IsUnit (diagonal v) ↔ IsUnit v := by + simp only [← nonempty_invertible_iff_isUnit, + (diagonal_invertible_equiv_invertible v).nonempty_congr] +#align matrix.is_unit_diagonal Matrix.isUnit_diagonal + +theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse v) := + by + rw [nonsing_inv_eq_ring_inverse] + by_cases h : IsUnit v + · have := is_unit_diagonal.mpr h + cases this.nonempty_invertible + cases h.nonempty_invertible + rw [Ring.inverse_invertible, Ring.inverse_invertible, inv_of_diagonal_eq] + · have := is_unit_diagonal.not.mpr h + rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this] +#align matrix.inv_diagonal Matrix.inv_diagonal + +end Diagonal + +@[simp] +theorem inv_inv_inv (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ := + by + by_cases h : IsUnit A.det + · rw [nonsing_inv_nonsing_inv _ h] + · simp [nonsing_inv_apply_not_is_unit _ h] +#align matrix.inv_inv_inv Matrix.inv_inv_inv + +theorem mul_inv_rev (A B : Matrix n n α) : (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹ := + by + simp only [inv_def] + rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib, + Ring.mul_inverse_rev] +#align matrix.mul_inv_rev Matrix.mul_inv_rev + +/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ +/-- A version of `list.prod_inv_reverse` for `matrix.has_inv`. -/ +theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.Prod⁻¹ = (l.reverse.map Inv.inv).Prod + | [] => by rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one] + | A::Xs => by + rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons, Matrix.mul_eq_mul, + Matrix.mul_eq_mul, mul_inv_rev, list_prod_inv_reverse] +#align matrix.list_prod_inv_reverse Matrix.list_prod_inv_reverse + +/-- One form of **Cramer's rule**. See `matrix.mul_vec_cramer` for a stronger form. -/ +@[simp] +theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : + A.det • A⁻¹.mulVec b = cramer A b := by + rw [cramer_eq_adjugate_mul_vec, A.nonsing_inv_apply h, ← smul_mul_vec_assoc, smul_smul, + h.mul_coe_inv, one_smul] +#align matrix.det_smul_inv_mul_vec_eq_cramer Matrix.det_smul_inv_mulVec_eq_cramer + +/-- One form of **Cramer's rule**. See `matrix.mul_vec_cramer` for a stronger form. -/ +@[simp] +theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : + A.det • A⁻¹.vecMul b = cramer Aᵀ b := by + rw [← A⁻¹.transpose_transpose, vec_mul_transpose, transpose_nonsing_inv, ← det_transpose, + Aᵀ.det_smul_inv_mulVec_eq_cramer _ (is_unit_det_transpose A h)] +#align matrix.det_smul_inv_vec_mul_eq_cramer_transpose Matrix.det_smul_inv_vecMul_eq_cramer_transpose + +/-! ### Inverses of permutated matrices + +Note that the simp-normal form of `matrix.reindex` is `matrix.submatrix`, so we prove most of these +results about only the latter. +-/ + + +section Submatrix + +variable [Fintype m] + +variable [DecidableEq m] + +/-- `A.submatrix e₁ e₂` is invertible if `A` is -/ +def submatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] : + Invertible (A.submatrix e₁ e₂) := + invertibleOfRightInverse _ ((⅟ A).submatrix e₂ e₁) <| by + rw [Matrix.submatrix_mul_equiv, Matrix.mul_invOf_self, submatrix_one_equiv] +#align matrix.submatrix_equiv_invertible Matrix.submatrixEquivInvertible + +/-- `A` is invertible if `A.submatrix e₁ e₂` is -/ +def invertibleOfSubmatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) + [Invertible (A.submatrix e₁ e₂)] : Invertible A := + invertibleOfRightInverse _ ((⅟ (A.submatrix e₁ e₂)).submatrix e₂.symm e₁.symm) <| + by + have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by simp + conv in _ ⬝ _ => + congr + rw [this] + rw [Matrix.submatrix_mul_equiv, Matrix.mul_invOf_self, submatrix_one_equiv] +#align matrix.invertible_of_submatrix_equiv_invertible Matrix.invertibleOfSubmatrixEquivInvertible + +theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] + [Invertible (A.submatrix e₁ e₂)] : ⅟ (A.submatrix e₁ e₂) = (⅟ A).submatrix e₂ e₁ := + by + letI := submatrix_equiv_invertible A e₁ e₂ + haveI := Invertible.subsingleton (A.submatrix e₁ e₂) + convert(rfl : ⅟ (A.submatrix e₁ e₂) = _) +#align matrix.inv_of_submatrix_equiv_eq Matrix.invOf_submatrix_equiv_eq + +/-- Together `matrix.submatrix_equiv_invertible` and +`matrix.invertible_of_submatrix_equiv_invertible` form an equivalence, although both sides of the +equiv are subsingleton anyway. -/ +@[simps] +def submatrixEquivInvertibleEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) : + Invertible (A.submatrix e₁ e₂) ≃ Invertible A + where + toFun _ := invertible_of_submatrix_equiv_invertible A e₁ e₂ + invFun _ := submatrix_equiv_invertible A e₁ e₂ + left_inv _ := Subsingleton.elim _ _ + right_inv _ := Subsingleton.elim _ _ +#align matrix.submatrix_equiv_invertible_equiv_invertible Matrix.submatrixEquivInvertibleEquivInvertible + +/-- When lowered to a prop, `matrix.invertible_of_submatrix_equiv_invertible` forms an `iff`. -/ +@[simp] +theorem isUnit_submatrix_equiv {A : Matrix m m α} (e₁ e₂ : n ≃ m) : + IsUnit (A.submatrix e₁ e₂) ↔ IsUnit A := by + simp only [← nonempty_invertible_iff_isUnit, + (submatrix_equiv_invertible_equiv_invertible A _ _).nonempty_congr] +#align matrix.is_unit_submatrix_equiv Matrix.isUnit_submatrix_equiv + +@[simp] +theorem inv_submatrix_equiv (A : Matrix m m α) (e₁ e₂ : n ≃ m) : + (A.submatrix e₁ e₂)⁻¹ = A⁻¹.submatrix e₂ e₁ := + by + by_cases h : IsUnit A + · cases h.nonempty_invertible + letI := submatrix_equiv_invertible A e₁ e₂ + rw [← inv_of_eq_nonsing_inv, ← inv_of_eq_nonsing_inv, inv_of_submatrix_equiv_eq] + · have := (is_unit_submatrix_equiv e₁ e₂).Not.mpr h + simp_rw [nonsing_inv_eq_ring_inverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this, + submatrix_zero, Pi.zero_apply] +#align matrix.inv_submatrix_equiv Matrix.inv_submatrix_equiv + +theorem inv_reindex (e₁ e₂ : n ≃ m) (A : Matrix n n α) : (reindex e₁ e₂ A)⁻¹ = reindex e₂ e₁ A⁻¹ := + inv_submatrix_equiv A e₁.symm e₂.symm +#align matrix.inv_reindex Matrix.inv_reindex + +end Submatrix + +/-! ### More results about determinants -/ + + +section Det + +variable [Fintype m] [DecidableEq m] + +/-- A variant of `matrix.det_units_conj`. -/ +theorem det_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : det (M ⬝ N ⬝ M⁻¹) = det N := + by rw [← h.unit_spec, ← coe_units_inv, det_units_conj] +#align matrix.det_conj Matrix.det_conj + +/-- A variant of `matrix.det_units_conj'`. -/ +theorem det_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : + det (M⁻¹ ⬝ N ⬝ M) = det N := by rw [← h.unit_spec, ← coe_units_inv, det_units_conj'] +#align matrix.det_conj' Matrix.det_conj' + +end Det + +end Matrix + From 3c50d41f96b0d70cb0b7d0b2fb0ba404740478b9 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 25 Apr 2023 12:02:53 +0200 Subject: [PATCH 3/8] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + .../Matrix/NonsingularInverse.lean | 101 ++++++------------ 2 files changed, 35 insertions(+), 67 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 5fe043ec5f925..86da1953375c8 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1403,6 +1403,7 @@ import Mathlib.LinearAlgebra.Matrix.Determinant import Mathlib.LinearAlgebra.Matrix.DotProduct import Mathlib.LinearAlgebra.Matrix.MvPolynomial import Mathlib.LinearAlgebra.Matrix.Nondegenerate +import Mathlib.LinearAlgebra.Matrix.NonsingularInverse import Mathlib.LinearAlgebra.Matrix.Orthogonal import Mathlib.LinearAlgebra.Matrix.Polynomial import Mathlib.LinearAlgebra.Matrix.Reindex diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index c8e3d986b97a6..75ac76d6bd453 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -8,7 +8,7 @@ Authors: Tim Baanen, Lu-Ming Zhang ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.LinearAlgebra.Matrix.Adjugate +import Mathlib.LinearAlgebra.Matrix.Adjugate /-! # Nonsingular inverses @@ -102,8 +102,7 @@ protected theorem mul_mul_invOf_self_cancel (A : Matrix m n α) (B : Matrix n n variable (A : Matrix n n α) (B : Matrix n n α) /-- If `A.det` has a constructive inverse, produce one for `A`. -/ -def invertibleOfDetInvertible [Invertible A.det] : Invertible A - where +def invertibleOfDetInvertible [Invertible A.det] : Invertible A where invOf := ⅟ A.det • A.adjugate mul_invOf_self := by rw [mul_smul_comm, Matrix.mul_eq_mul, mul_adjugate, smul_smul, invOf_mul_self, one_smul] @@ -111,23 +110,20 @@ def invertibleOfDetInvertible [Invertible A.det] : Invertible A rw [smul_mul_assoc, Matrix.mul_eq_mul, adjugate_mul, smul_smul, invOf_mul_self, one_smul] #align matrix.invertible_of_det_invertible Matrix.invertibleOfDetInvertible -theorem invOf_eq [Invertible A.det] [Invertible A] : ⅟ A = ⅟ A.det • A.adjugate := - by +theorem invOf_eq [Invertible A.det] [Invertible A] : ⅟ A = ⅟ A.det • A.adjugate := by letI := invertible_of_det_invertible A convert(rfl : ⅟ A = _) #align matrix.inv_of_eq Matrix.invOf_eq /-- `A.det` is invertible if `A` has a left inverse. -/ -def detInvertibleOfLeftInverse (h : B ⬝ A = 1) : Invertible A.det - where +def detInvertibleOfLeftInverse (h : B ⬝ A = 1) : Invertible A.det where invOf := B.det mul_invOf_self := by rw [mul_comm, ← det_mul, h, det_one] invOf_mul_self := by rw [← det_mul, h, det_one] #align matrix.det_invertible_of_left_inverse Matrix.detInvertibleOfLeftInverse /-- `A.det` is invertible if `A` has a right inverse. -/ -def detInvertibleOfRightInverse (h : A ⬝ B = 1) : Invertible A.det - where +def detInvertibleOfRightInverse (h : A ⬝ B = 1) : Invertible A.det where invOf := B.det mul_invOf_self := by rw [← det_mul, h, det_one] invOf_mul_self := by rw [mul_comm, ← det_mul, h, det_one] @@ -138,8 +134,7 @@ def detInvertibleOfInvertible [Invertible A] : Invertible A.det := detInvertibleOfLeftInverse A (⅟ A) (invOf_mul_self _) #align matrix.det_invertible_of_invertible Matrix.detInvertibleOfInvertible -theorem det_invOf [Invertible A] [Invertible A.det] : (⅟ A).det = ⅟ A.det := - by +theorem det_invOf [Invertible A] [Invertible A.det] : (⅟ A).det = ⅟ A.det := by letI := det_invertible_of_invertible A convert(rfl : _ = ⅟ A.det) #align matrix.det_inv_of Matrix.det_invOf @@ -147,8 +142,7 @@ theorem det_invOf [Invertible A] [Invertible A.det] : (⅟ A).det = ⅟ A.det := /-- Together `matrix.det_invertible_of_invertible` and `matrix.invertible_of_det_invertible` form an equivalence, although both sides of the equiv are subsingleton anyway. -/ @[simps] -def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det - where +def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det where toFun := @detInvertibleOfInvertible _ _ _ _ _ A invFun := @invertibleOfDetInvertible _ _ _ _ _ A left_inv _ := Subsingleton.elim _ _ @@ -189,15 +183,13 @@ instance invertibleTranspose [Invertible A] : Invertible Aᵀ := #align matrix.invertible_transpose Matrix.invertibleTranspose /-- A matrix is invertible if the transpose is invertible. -/ -def invertibleOfInvertibleTranspose [Invertible Aᵀ] : Invertible A := - by +def invertibleOfInvertibleTranspose [Invertible Aᵀ] : Invertible A := by rw [← transpose_transpose A] infer_instance #align matrix.invertible__of_invertible_transpose Matrix.invertibleOfInvertibleTranspose /-- A matrix is invertible if the conjugate transpose is invertible. -/ -def invertibleOfInvertibleConjTranspose [StarRing α] [Invertible Aᴴ] : Invertible A := - by +def invertibleOfInvertibleConjTranspose [StarRing α] [Invertible Aᴴ] : Invertible A := by rw [← conj_transpose_conj_transpose A] infer_instance #align matrix.invertible_of_invertible_conj_transpose Matrix.invertibleOfInvertibleConjTranspose @@ -251,8 +243,7 @@ variable [Fintype n] [DecidableEq n] [CommRing α] variable (A : Matrix n n α) (B : Matrix n n α) -theorem isUnit_det_transpose (h : IsUnit A.det) : IsUnit Aᵀ.det := - by +theorem isUnit_det_transpose (h : IsUnit A.det) : IsUnit Aᵀ.det := by rw [det_transpose] exact h #align matrix.is_unit_det_transpose Matrix.isUnit_det_transpose @@ -278,8 +269,7 @@ theorem nonsing_inv_apply (h : IsUnit A.det) : A⁻¹ = (↑h.Unit⁻¹ : α) /-- The nonsingular inverse is the same as `inv_of` when `A` is invertible. -/ @[simp] -theorem invOf_eq_nonsing_inv [Invertible A] : ⅟ A = A⁻¹ := - by +theorem invOf_eq_nonsing_inv [Invertible A] : ⅟ A = A⁻¹ := by letI := det_invertible_of_invertible A rw [inv_def, Ring.inverse_invertible, inv_of_eq] #align matrix.inv_of_eq_nonsing_inv Matrix.invOf_eq_nonsing_inv @@ -287,15 +277,13 @@ theorem invOf_eq_nonsing_inv [Invertible A] : ⅟ A = A⁻¹ := /-- Coercing the result of `units.has_inv` is the same as coercing first and applying the nonsingular inverse. -/ @[simp, norm_cast] -theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α) := - by +theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α) := by letI := A.invertible rw [← inv_of_eq_nonsing_inv, invOf_units] #align matrix.coe_units_inv Matrix.coe_units_inv /-- The nonsingular inverse is the same as the general `ring.inverse`. -/ -theorem nonsing_inv_eq_ring_inverse : A⁻¹ = Ring.inverse A := - by +theorem nonsing_inv_eq_ring_inverse : A⁻¹ = Ring.inverse A := by by_cases h_det : IsUnit A.det · cases (A.is_unit_iff_is_unit_det.mpr h_det).nonempty_invertible rw [← inv_of_eq_nonsing_inv, Ring.inverse_invertible] @@ -314,22 +302,19 @@ theorem conjTranspose_nonsing_inv [StarRing α] : A⁻¹ᴴ = Aᴴ⁻¹ := by /-- The `nonsing_inv` of `A` is a right inverse. -/ @[simp] -theorem mul_nonsing_inv (h : IsUnit A.det) : A ⬝ A⁻¹ = 1 := - by +theorem mul_nonsing_inv (h : IsUnit A.det) : A ⬝ A⁻¹ = 1 := by cases (A.is_unit_iff_is_unit_det.mpr h).nonempty_invertible rw [← inv_of_eq_nonsing_inv, Matrix.mul_invOf_self] #align matrix.mul_nonsing_inv Matrix.mul_nonsing_inv /-- The `nonsing_inv` of `A` is a left inverse. -/ @[simp] -theorem nonsing_inv_mul (h : IsUnit A.det) : A⁻¹ ⬝ A = 1 := - by +theorem nonsing_inv_mul (h : IsUnit A.det) : A⁻¹ ⬝ A = 1 := by cases (A.is_unit_iff_is_unit_det.mpr h).nonempty_invertible rw [← inv_of_eq_nonsing_inv, Matrix.invOf_mul_self] #align matrix.nonsing_inv_mul Matrix.nonsing_inv_mul -instance [Invertible A] : Invertible A⁻¹ := - by +instance [Invertible A] : Invertible A⁻¹ := by rw [← inv_of_eq_nonsing_inv] infer_instance @@ -400,8 +385,7 @@ theorem mul_inv_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible rw [h, mul_inv_cancel_right_of_invertible]⟩ #align matrix.mul_inv_eq_iff_eq_mul_of_invertible Matrix.mul_inv_eq_iff_eq_mul_of_invertible -theorem nonsing_inv_cancel_or_zero : A⁻¹ ⬝ A = 1 ∧ A ⬝ A⁻¹ = 1 ∨ A⁻¹ = 0 := - by +theorem nonsing_inv_cancel_or_zero : A⁻¹ ⬝ A = 1 ∧ A ⬝ A⁻¹ = 1 ∨ A⁻¹ = 0 := by by_cases h : IsUnit A.det · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩ · exact Or.inr (nonsing_inv_apply_not_is_unit _ h) @@ -412,8 +396,7 @@ theorem det_nonsing_inv_mul_det (h : IsUnit A.det) : A⁻¹.det * A.det = 1 := b #align matrix.det_nonsing_inv_mul_det Matrix.det_nonsing_inv_mul_det @[simp] -theorem det_nonsing_inv : A⁻¹.det = Ring.inverse A.det := - by +theorem det_nonsing_inv : A⁻¹.det = Ring.inverse A.det := by by_cases h : IsUnit A.det · cases h.nonempty_invertible letI := invertible_of_det_invertible A @@ -455,8 +438,7 @@ noncomputable def nonsingInvUnit (h : IsUnit A.det) : (Matrix n n α)ˣ := #align matrix.nonsing_inv_unit Matrix.nonsingInvUnit theorem unitOfDetInvertible_eq_nonsingInvUnit [Invertible A.det] : - unitOfDetInvertible A = nonsingInvUnit A (isUnit_of_invertible _) := - by + unitOfDetInvertible A = nonsingInvUnit A (isUnit_of_invertible _) := by ext rfl #align matrix.unit_of_det_invertible_eq_nonsing_inv_unit Matrix.unitOfDetInvertible_eq_nonsingInvUnit @@ -493,8 +475,7 @@ theorem right_inv_eq_left_inv (h : A ⬝ B = 1) (g : C ⬝ A = 1) : B = C := by rw [← inv_eq_right_inv h, ← inv_eq_left_inv g] #align matrix.right_inv_eq_left_inv Matrix.right_inv_eq_left_inv -theorem inv_inj (h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) : A = B := - by +theorem inv_inj (h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) : A = B := by refine' left_inv_eq_left_inv (mul_nonsing_inv _ h') _ rw [h] refine' mul_nonsing_inv _ _ @@ -506,8 +487,7 @@ end InvEqInv variable (A) @[simp] -theorem inv_zero : (0 : Matrix n n α)⁻¹ = 0 := - by +theorem inv_zero : (0 : Matrix n n α)⁻¹ = 0 := by cases' subsingleton_or_nontrivial α with ht ht · simp cases' (Fintype.card n).zero_le.eq_or_lt with hc hc @@ -531,8 +511,7 @@ theorem inv_smul' (k : αˣ) (h : IsUnit A.det) : (k • A)⁻¹ = k⁻¹ • A inv_eq_left_inv (by simp [h, smul_smul]) #align matrix.inv_smul' Matrix.inv_smul' -theorem inv_adjugate (A : Matrix n n α) (h : IsUnit A.det) : (adjugate A)⁻¹ = h.Unit⁻¹ • A := - by +theorem inv_adjugate (A : Matrix n n α) (h : IsUnit A.det) : (adjugate A)⁻¹ = h.Unit⁻¹ • A := by refine' inv_eq_left_inv _ rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.coe_inv_mul, one_smul] #align matrix.inv_adjugate Matrix.inv_adjugate @@ -546,28 +525,24 @@ def diagonalInvertible {α} [NonAssocSemiring α] (v : n → α) [Invertible v] #align matrix.diagonal_invertible Matrix.diagonalInvertible theorem invOf_diagonal_eq {α} [Semiring α] (v : n → α) [Invertible v] [Invertible (diagonal v)] : - ⅟ (diagonal v) = diagonal (⅟ v) := - by + ⅟ (diagonal v) = diagonal (⅟ v) := by letI := diagonal_invertible v haveI := Invertible.subsingleton (diagonal v) convert(rfl : ⅟ (diagonal v) = _) #align matrix.inv_of_diagonal_eq Matrix.invOf_diagonal_eq /-- `v` is invertible if `diagonal v` is -/ -def invertibleOfDiagonalInvertible (v : n → α) [Invertible (diagonal v)] : Invertible v - where +def invertibleOfDiagonalInvertible (v : n → α) [Invertible (diagonal v)] : Invertible v where invOf := diag (⅟ (diagonal v)) invOf_mul_self := - funext fun i => - by + funext fun i => by letI : Invertible (diagonal v).det := det_invertible_of_invertible _ rw [inv_of_eq, diag_smul, adjugate_diagonal, diag_diagonal] dsimp rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal] exact mul_invOf_self _ mul_invOf_self := - funext fun i => - by + funext fun i => by letI : Invertible (diagonal v).det := det_invertible_of_invertible _ rw [inv_of_eq, diag_smul, adjugate_diagonal, diag_diagonal] dsimp @@ -578,8 +553,7 @@ def invertibleOfDiagonalInvertible (v : n → α) [Invertible (diagonal v)] : In /-- Together `matrix.diagonal_invertible` and `matrix.invertible_of_diagonal_invertible` form an equivalence, although both sides of the equiv are subsingleton anyway. -/ @[simps] -def diagonalInvertibleEquivInvertible (v : n → α) : Invertible (diagonal v) ≃ Invertible v - where +def diagonalInvertibleEquivInvertible (v : n → α) : Invertible (diagonal v) ≃ Invertible v where toFun := @invertibleOfDiagonalInvertible _ _ _ _ _ _ invFun := @diagonalInvertible _ _ _ _ _ _ left_inv _ := Subsingleton.elim _ _ @@ -593,8 +567,7 @@ theorem isUnit_diagonal {v : n → α} : IsUnit (diagonal v) ↔ IsUnit v := by (diagonal_invertible_equiv_invertible v).nonempty_congr] #align matrix.is_unit_diagonal Matrix.isUnit_diagonal -theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse v) := - by +theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse v) := by rw [nonsing_inv_eq_ring_inverse] by_cases h : IsUnit v · have := is_unit_diagonal.mpr h @@ -608,15 +581,13 @@ theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse end Diagonal @[simp] -theorem inv_inv_inv (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ := - by +theorem inv_inv_inv (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ := by by_cases h : IsUnit A.det · rw [nonsing_inv_nonsing_inv _ h] · simp [nonsing_inv_apply_not_is_unit _ h] #align matrix.inv_inv_inv Matrix.inv_inv_inv -theorem mul_inv_rev (A B : Matrix n n α) : (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹ := - by +theorem mul_inv_rev (A B : Matrix n n α) : (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹ := by simp only [inv_def] rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib, Ring.mul_inverse_rev] @@ -670,8 +641,7 @@ def submatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertib /-- `A` is invertible if `A.submatrix e₁ e₂` is -/ def invertibleOfSubmatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible (A.submatrix e₁ e₂)] : Invertible A := - invertibleOfRightInverse _ ((⅟ (A.submatrix e₁ e₂)).submatrix e₂.symm e₁.symm) <| - by + invertibleOfRightInverse _ ((⅟ (A.submatrix e₁ e₂)).submatrix e₂.symm e₁.symm) <| by have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by simp conv in _ ⬝ _ => congr @@ -680,8 +650,7 @@ def invertibleOfSubmatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ #align matrix.invertible_of_submatrix_equiv_invertible Matrix.invertibleOfSubmatrixEquivInvertible theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] - [Invertible (A.submatrix e₁ e₂)] : ⅟ (A.submatrix e₁ e₂) = (⅟ A).submatrix e₂ e₁ := - by + [Invertible (A.submatrix e₁ e₂)] : ⅟ (A.submatrix e₁ e₂) = (⅟ A).submatrix e₂ e₁ := by letI := submatrix_equiv_invertible A e₁ e₂ haveI := Invertible.subsingleton (A.submatrix e₁ e₂) convert(rfl : ⅟ (A.submatrix e₁ e₂) = _) @@ -692,8 +661,7 @@ theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Inve equiv are subsingleton anyway. -/ @[simps] def submatrixEquivInvertibleEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) : - Invertible (A.submatrix e₁ e₂) ≃ Invertible A - where + Invertible (A.submatrix e₁ e₂) ≃ Invertible A where toFun _ := invertible_of_submatrix_equiv_invertible A e₁ e₂ invFun _ := submatrix_equiv_invertible A e₁ e₂ left_inv _ := Subsingleton.elim _ _ @@ -710,8 +678,7 @@ theorem isUnit_submatrix_equiv {A : Matrix m m α} (e₁ e₂ : n ≃ m) : @[simp] theorem inv_submatrix_equiv (A : Matrix m m α) (e₁ e₂ : n ≃ m) : - (A.submatrix e₁ e₂)⁻¹ = A⁻¹.submatrix e₂ e₁ := - by + (A.submatrix e₁ e₂)⁻¹ = A⁻¹.submatrix e₂ e₁ := by by_cases h : IsUnit A · cases h.nonempty_invertible letI := submatrix_equiv_invertible A e₁ e₂ From 9f59d4897ffaa4dc003801596766261edb54e876 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 25 Apr 2023 12:19:36 +0200 Subject: [PATCH 4/8] Initial fixes --- .../Matrix/NonsingularInverse.lean | 118 +++++++++--------- 1 file changed, 59 insertions(+), 59 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 75ac76d6bd453..7f249bc98e6ee 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -111,7 +111,7 @@ def invertibleOfDetInvertible [Invertible A.det] : Invertible A where #align matrix.invertible_of_det_invertible Matrix.invertibleOfDetInvertible theorem invOf_eq [Invertible A.det] [Invertible A] : ⅟ A = ⅟ A.det • A.adjugate := by - letI := invertible_of_det_invertible A + letI := invertibleOfDetInvertible A convert(rfl : ⅟ A = _) #align matrix.inv_of_eq Matrix.invOf_eq @@ -135,7 +135,7 @@ def detInvertibleOfInvertible [Invertible A] : Invertible A.det := #align matrix.det_invertible_of_invertible Matrix.detInvertibleOfInvertible theorem det_invOf [Invertible A] [Invertible A.det] : (⅟ A).det = ⅟ A.det := by - letI := det_invertible_of_invertible A + letI := detInvertibleOfInvertible A convert(rfl : _ = ⅟ A.det) #align matrix.det_inv_of Matrix.det_invOf @@ -154,14 +154,14 @@ variable {A B} theorem mul_eq_one_comm : A ⬝ B = 1 ↔ B ⬝ A = 1 := suffices ∀ A B, A ⬝ B = 1 → B ⬝ A = 1 from ⟨this A B, this B A⟩ fun A B h => by - letI : Invertible B.det := det_invertible_of_left_inverse _ _ h - letI : Invertible B := invertible_of_det_invertible B + letI : Invertible B.det := detInvertibleOfLeftInverse _ _ h + letI : Invertible B := invertibleOfDetInvertible B calc B ⬝ A = B ⬝ A ⬝ (B ⬝ ⅟ B) := by rw [Matrix.mul_invOf_self, Matrix.mul_one] _ = B ⬝ (A ⬝ B ⬝ ⅟ B) := by simp only [Matrix.mul_assoc] _ = B ⬝ ⅟ B := by rw [h, Matrix.one_mul] _ = 1 := Matrix.mul_invOf_self B - + #align matrix.mul_eq_one_comm Matrix.mul_eq_one_comm variable (A B) @@ -178,8 +178,8 @@ def invertibleOfRightInverse (h : A ⬝ B = 1) : Invertible A := /-- The transpose of an invertible matrix is invertible. -/ instance invertibleTranspose [Invertible A] : Invertible Aᵀ := - haveI : Invertible Aᵀ.det := by simpa using det_invertible_of_invertible A - invertible_of_det_invertible Aᵀ + haveI : Invertible Aᵀ.det := by simpa using detInvertibleOfInvertible A + invertibleOfDetInvertible Aᵀ #align matrix.invertible_transpose Matrix.invertibleTranspose /-- A matrix is invertible if the transpose is invertible. -/ @@ -190,7 +190,7 @@ def invertibleOfInvertibleTranspose [Invertible Aᵀ] : Invertible A := by /-- A matrix is invertible if the conjugate transpose is invertible. -/ def invertibleOfInvertibleConjTranspose [StarRing α] [Invertible Aᴴ] : Invertible A := by - rw [← conj_transpose_conj_transpose A] + rw [← conjTranspose_conjTranspose A] infer_instance #align matrix.invertible_of_invertible_conj_transpose Matrix.invertibleOfInvertibleConjTranspose @@ -201,7 +201,7 @@ def unitOfDetInvertible [Invertible A.det] : (Matrix n n α)ˣ := /-- When lowered to a prop, `matrix.invertible_equiv_det_invertible` forms an `iff`. -/ theorem isUnit_iff_isUnit_det : IsUnit A ↔ IsUnit A.det := by - simp only [← nonempty_invertible_iff_isUnit, (invertible_equiv_det_invertible A).nonempty_congr] + simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivDetInvertible A).nonempty_congr] #align matrix.is_unit_iff_is_unit_det Matrix.isUnit_iff_isUnit_det /-! #### Variants of the statements above with `is_unit`-/ @@ -230,11 +230,11 @@ theorem isUnit_det_of_right_inverse (h : A ⬝ B = 1) : IsUnit A.det := #align matrix.is_unit_det_of_right_inverse Matrix.isUnit_det_of_right_inverse theorem det_ne_zero_of_left_inverse [Nontrivial α] (h : B ⬝ A = 1) : A.det ≠ 0 := - (isUnit_det_of_left_inverse h).NeZero + (isUnit_det_of_left_inverse h).ne_zero #align matrix.det_ne_zero_of_left_inverse Matrix.det_ne_zero_of_left_inverse theorem det_ne_zero_of_right_inverse [Nontrivial α] (h : A ⬝ B = 1) : A.det ≠ 0 := - (isUnit_det_of_right_inverse h).NeZero + (isUnit_det_of_right_inverse h).ne_zero #align matrix.det_ne_zero_of_right_inverse Matrix.det_ne_zero_of_right_inverse end Invertible @@ -252,7 +252,7 @@ theorem isUnit_det_transpose (h : IsUnit A.det) : IsUnit Aᵀ.det := by /-- The inverse of a square matrix, when it is invertible (and zero otherwise).-/ -noncomputable instance : Inv (Matrix n n α) := +noncomputable instance inv : Inv (Matrix n n α) := ⟨fun A => Ring.inverse A.det • A.adjugate⟩ theorem inv_def (A : Matrix n n α) : A⁻¹ = Ring.inverse A.det • A.adjugate := @@ -263,15 +263,15 @@ theorem nonsing_inv_apply_not_isUnit (h : ¬IsUnit A.det) : A⁻¹ = 0 := by rw [inv_def, Ring.inverse_non_unit _ h, zero_smul] #align matrix.nonsing_inv_apply_not_is_unit Matrix.nonsing_inv_apply_not_isUnit -theorem nonsing_inv_apply (h : IsUnit A.det) : A⁻¹ = (↑h.Unit⁻¹ : α) • A.adjugate := by +theorem nonsing_inv_apply (h : IsUnit A.det) : A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate := by rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec] #align matrix.nonsing_inv_apply Matrix.nonsing_inv_apply /-- The nonsingular inverse is the same as `inv_of` when `A` is invertible. -/ @[simp] theorem invOf_eq_nonsing_inv [Invertible A] : ⅟ A = A⁻¹ := by - letI := det_invertible_of_invertible A - rw [inv_def, Ring.inverse_invertible, inv_of_eq] + letI := detInvertibleOfInvertible A + rw [inv_def, Ring.inverse_invertible, invOf_eq] #align matrix.inv_of_eq_nonsing_inv Matrix.invOf_eq_nonsing_inv /-- Coercing the result of `units.has_inv` is the same as coercing first and applying the @@ -279,48 +279,49 @@ nonsingular inverse. -/ @[simp, norm_cast] theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α) := by letI := A.invertible - rw [← inv_of_eq_nonsing_inv, invOf_units] + rw [← invOf_eq_nonsing_inv, invOf_units] #align matrix.coe_units_inv Matrix.coe_units_inv /-- The nonsingular inverse is the same as the general `ring.inverse`. -/ theorem nonsing_inv_eq_ring_inverse : A⁻¹ = Ring.inverse A := by by_cases h_det : IsUnit A.det - · cases (A.is_unit_iff_is_unit_det.mpr h_det).nonempty_invertible - rw [← inv_of_eq_nonsing_inv, Ring.inverse_invertible] - · have h := mt A.is_unit_iff_is_unit_det.mp h_det - rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_is_unit A h_det] + · cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible + rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible] + · have h := mt A.isUnit_iff_isUnit_det.mp h_det + rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det] #align matrix.nonsing_inv_eq_ring_inverse Matrix.nonsing_inv_eq_ring_inverse theorem transpose_nonsing_inv : A⁻¹ᵀ = Aᵀ⁻¹ := by rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose] #align matrix.transpose_nonsing_inv Matrix.transpose_nonsing_inv +set_option synthInstance.etaExperiment true in theorem conjTranspose_nonsing_inv [StarRing α] : A⁻¹ᴴ = Aᴴ⁻¹ := by - rw [inv_def, inv_def, conj_transpose_smul, det_conj_transpose, adjugate_conj_transpose, + rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose, Ring.inverse_star] #align matrix.conj_transpose_nonsing_inv Matrix.conjTranspose_nonsing_inv /-- The `nonsing_inv` of `A` is a right inverse. -/ @[simp] theorem mul_nonsing_inv (h : IsUnit A.det) : A ⬝ A⁻¹ = 1 := by - cases (A.is_unit_iff_is_unit_det.mpr h).nonempty_invertible - rw [← inv_of_eq_nonsing_inv, Matrix.mul_invOf_self] + cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible + rw [← invOf_eq_nonsing_inv, Matrix.mul_invOf_self] #align matrix.mul_nonsing_inv Matrix.mul_nonsing_inv /-- The `nonsing_inv` of `A` is a left inverse. -/ @[simp] theorem nonsing_inv_mul (h : IsUnit A.det) : A⁻¹ ⬝ A = 1 := by - cases (A.is_unit_iff_is_unit_det.mpr h).nonempty_invertible - rw [← inv_of_eq_nonsing_inv, Matrix.invOf_mul_self] + cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible + rw [← invOf_eq_nonsing_inv, Matrix.invOf_mul_self] #align matrix.nonsing_inv_mul Matrix.nonsing_inv_mul instance [Invertible A] : Invertible A⁻¹ := by - rw [← inv_of_eq_nonsing_inv] + rw [← invOf_eq_nonsing_inv] infer_instance @[simp] theorem inv_inv_of_invertible [Invertible A] : A⁻¹⁻¹ = A := by - simp only [← inv_of_eq_nonsing_inv, invOf_invOf] + simp only [← invOf_eq_nonsing_inv, invOf_invOf] #align matrix.inv_inv_of_invertible Matrix.inv_inv_of_invertible @[simp] @@ -388,7 +389,7 @@ theorem mul_inv_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible theorem nonsing_inv_cancel_or_zero : A⁻¹ ⬝ A = 1 ∧ A ⬝ A⁻¹ = 1 ∨ A⁻¹ = 0 := by by_cases h : IsUnit A.det · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩ - · exact Or.inr (nonsing_inv_apply_not_is_unit _ h) + · exact Or.inr (nonsing_inv_apply_not_isUnit _ h) #align matrix.nonsing_inv_cancel_or_zero Matrix.nonsing_inv_cancel_or_zero theorem det_nonsing_inv_mul_det (h : IsUnit A.det) : A⁻¹.det * A.det = 1 := by @@ -399,11 +400,11 @@ theorem det_nonsing_inv_mul_det (h : IsUnit A.det) : A⁻¹.det * A.det = 1 := b theorem det_nonsing_inv : A⁻¹.det = Ring.inverse A.det := by by_cases h : IsUnit A.det · cases h.nonempty_invertible - letI := invertible_of_det_invertible A - rw [Ring.inverse_invertible, ← inv_of_eq_nonsing_inv, det_inv_of] + letI := invertibleOfDetInvertible A + rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf] cases isEmpty_or_nonempty n - · rw [det_is_empty, det_is_empty, Ring.inverse_one] - · rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_is_unit _ h, det_zero ‹_›] + · rw [det_isEmpty, det_isEmpty, Ring.inverse_one] + · rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›] #align matrix.det_nonsing_inv Matrix.det_nonsing_inv theorem isUnit_nonsing_inv_det (h : IsUnit A.det) : IsUnit A⁻¹.det := @@ -416,8 +417,8 @@ theorem nonsing_inv_nonsing_inv (h : IsUnit A.det) : A⁻¹⁻¹ = A := A⁻¹⁻¹ = 1 ⬝ A⁻¹⁻¹ := by rw [Matrix.one_mul] _ = A ⬝ A⁻¹ ⬝ A⁻¹⁻¹ := by rw [A.mul_nonsing_inv h] _ = A := by - rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.is_unit_nonsing_inv_det h), Matrix.mul_one] - + rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_one] + #align matrix.nonsing_inv_nonsing_inv Matrix.nonsing_inv_nonsing_inv theorem isUnit_nonsing_inv_det_iff {A : Matrix n n α} : IsUnit A⁻¹.det ↔ IsUnit A.det := by @@ -447,8 +448,8 @@ variable {A} {B} /-- If matrix A is left invertible, then its inverse equals its left inverse. -/ theorem inv_eq_left_inv (h : B ⬝ A = 1) : A⁻¹ = B := - letI := invertible_of_left_inverse _ _ h - inv_of_eq_nonsing_inv A ▸ invOf_eq_left_inv h + letI := invertibleOfLeftInverse _ _ h + invOf_eq_nonsing_inv A ▸ invOf_eq_left_inv h #align matrix.inv_eq_left_inv Matrix.inv_eq_left_inv /-- If matrix A is right invertible, then its inverse equals its right inverse. -/ @@ -479,7 +480,7 @@ theorem inv_inj (h : A⁻¹ = B⁻¹) (h' : IsUnit A.det) : A = B := by refine' left_inv_eq_left_inv (mul_nonsing_inv _ h') _ rw [h] refine' mul_nonsing_inv _ _ - rwa [← is_unit_nonsing_inv_det_iff, ← h, is_unit_nonsing_inv_det_iff] + rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff] #align matrix.inv_inj Matrix.inv_inj end InvEqInv @@ -495,13 +496,13 @@ theorem inv_zero : (0 : Matrix n n α)⁻¹ = 0 := by haveI := hc ext i exact (IsEmpty.false i).elim - · have hn : Nonempty n := fintype.card_pos_iff.mp hc - refine' nonsing_inv_apply_not_is_unit _ _ + · have hn : Nonempty n := Fintype.card_pos_iff.mp hc + refine' nonsing_inv_apply_not_isUnit _ _ simp [hn] #align matrix.inv_zero Matrix.inv_zero noncomputable instance : InvOneClass (Matrix n n α) := - { Matrix.hasOne, Matrix.hasInv with inv_one := inv_eq_left_inv (by simp) } + { Matrix.one, Matrix.inv with inv_one := inv_eq_left_inv (by simp) } theorem inv_smul (k : α) [Invertible k] (h : IsUnit A.det) : (k • A)⁻¹ = ⅟ k • A⁻¹ := inv_eq_left_inv (by simp [h, smul_smul]) @@ -511,9 +512,9 @@ theorem inv_smul' (k : αˣ) (h : IsUnit A.det) : (k • A)⁻¹ = k⁻¹ • A inv_eq_left_inv (by simp [h, smul_smul]) #align matrix.inv_smul' Matrix.inv_smul' -theorem inv_adjugate (A : Matrix n n α) (h : IsUnit A.det) : (adjugate A)⁻¹ = h.Unit⁻¹ • A := by +theorem inv_adjugate (A : Matrix n n α) (h : IsUnit A.det) : (adjugate A)⁻¹ = h.unit⁻¹ • A := by refine' inv_eq_left_inv _ - rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.coe_inv_mul, one_smul] + rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul] #align matrix.inv_adjugate Matrix.inv_adjugate section Diagonal @@ -526,7 +527,7 @@ def diagonalInvertible {α} [NonAssocSemiring α] (v : n → α) [Invertible v] theorem invOf_diagonal_eq {α} [Semiring α] (v : n → α) [Invertible v] [Invertible (diagonal v)] : ⅟ (diagonal v) = diagonal (⅟ v) := by - letI := diagonal_invertible v + letI := diagonalInvertible v haveI := Invertible.subsingleton (diagonal v) convert(rfl : ⅟ (diagonal v) = _) #align matrix.inv_of_diagonal_eq Matrix.invOf_diagonal_eq @@ -536,15 +537,15 @@ def invertibleOfDiagonalInvertible (v : n → α) [Invertible (diagonal v)] : In invOf := diag (⅟ (diagonal v)) invOf_mul_self := funext fun i => by - letI : Invertible (diagonal v).det := det_invertible_of_invertible _ - rw [inv_of_eq, diag_smul, adjugate_diagonal, diag_diagonal] + letI : Invertible (diagonal v).det := detInvertibleOfInvertible _ + rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal] dsimp rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal] exact mul_invOf_self _ mul_invOf_self := funext fun i => by - letI : Invertible (diagonal v).det := det_invertible_of_invertible _ - rw [inv_of_eq, diag_smul, adjugate_diagonal, diag_diagonal] + letI : Invertible (diagonal v).det := detInvertibleOfInvertible _ + rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal] dsimp rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal] exact mul_invOf_self _ @@ -570,11 +571,11 @@ theorem isUnit_diagonal {v : n → α} : IsUnit (diagonal v) ↔ IsUnit v := by theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse v) := by rw [nonsing_inv_eq_ring_inverse] by_cases h : IsUnit v - · have := is_unit_diagonal.mpr h + · have := isUnit_diagonal.mpr h cases this.nonempty_invertible cases h.nonempty_invertible rw [Ring.inverse_invertible, Ring.inverse_invertible, inv_of_diagonal_eq] - · have := is_unit_diagonal.not.mpr h + · have := isUnit_diagonal.not.mpr h rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this] #align matrix.inv_diagonal Matrix.inv_diagonal @@ -584,7 +585,7 @@ end Diagonal theorem inv_inv_inv (A : Matrix n n α) : A⁻¹⁻¹⁻¹ = A⁻¹ := by by_cases h : IsUnit A.det · rw [nonsing_inv_nonsing_inv _ h] - · simp [nonsing_inv_apply_not_is_unit _ h] + · simp [nonsing_inv_apply_not_isUnit _ h] #align matrix.inv_inv_inv Matrix.inv_inv_inv theorem mul_inv_rev (A B : Matrix n n α) : (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹ := by @@ -615,7 +616,7 @@ theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : Is theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • A⁻¹.vecMul b = cramer Aᵀ b := by rw [← A⁻¹.transpose_transpose, vec_mul_transpose, transpose_nonsing_inv, ← det_transpose, - Aᵀ.det_smul_inv_mulVec_eq_cramer _ (is_unit_det_transpose A h)] + Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)] #align matrix.det_smul_inv_vec_mul_eq_cramer_transpose Matrix.det_smul_inv_vecMul_eq_cramer_transpose /-! ### Inverses of permutated matrices @@ -651,7 +652,7 @@ def invertibleOfSubmatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] [Invertible (A.submatrix e₁ e₂)] : ⅟ (A.submatrix e₁ e₂) = (⅟ A).submatrix e₂ e₁ := by - letI := submatrix_equiv_invertible A e₁ e₂ + letI := submatrixEquivInvertible A e₁ e₂ haveI := Invertible.subsingleton (A.submatrix e₁ e₂) convert(rfl : ⅟ (A.submatrix e₁ e₂) = _) #align matrix.inv_of_submatrix_equiv_eq Matrix.invOf_submatrix_equiv_eq @@ -662,8 +663,8 @@ equiv are subsingleton anyway. -/ @[simps] def submatrixEquivInvertibleEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) : Invertible (A.submatrix e₁ e₂) ≃ Invertible A where - toFun _ := invertible_of_submatrix_equiv_invertible A e₁ e₂ - invFun _ := submatrix_equiv_invertible A e₁ e₂ + toFun _ := invertibleOfSubmatrixEquivInvertible A e₁ e₂ + invFun _ := submatrixEquivInvertible A e₁ e₂ left_inv _ := Subsingleton.elim _ _ right_inv _ := Subsingleton.elim _ _ #align matrix.submatrix_equiv_invertible_equiv_invertible Matrix.submatrixEquivInvertibleEquivInvertible @@ -673,7 +674,7 @@ def submatrixEquivInvertibleEquivInvertible (A : Matrix m m α) (e₁ e₂ : n theorem isUnit_submatrix_equiv {A : Matrix m m α} (e₁ e₂ : n ≃ m) : IsUnit (A.submatrix e₁ e₂) ↔ IsUnit A := by simp only [← nonempty_invertible_iff_isUnit, - (submatrix_equiv_invertible_equiv_invertible A _ _).nonempty_congr] + (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr] #align matrix.is_unit_submatrix_equiv Matrix.isUnit_submatrix_equiv @[simp] @@ -681,9 +682,9 @@ theorem inv_submatrix_equiv (A : Matrix m m α) (e₁ e₂ : n ≃ m) : (A.submatrix e₁ e₂)⁻¹ = A⁻¹.submatrix e₂ e₁ := by by_cases h : IsUnit A · cases h.nonempty_invertible - letI := submatrix_equiv_invertible A e₁ e₂ - rw [← inv_of_eq_nonsing_inv, ← inv_of_eq_nonsing_inv, inv_of_submatrix_equiv_eq] - · have := (is_unit_submatrix_equiv e₁ e₂).Not.mpr h + letI := submatrixEquivInvertible A e₁ e₂ + rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq] + · have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h simp_rw [nonsing_inv_eq_ring_inverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this, submatrix_zero, Pi.zero_apply] #align matrix.inv_submatrix_equiv Matrix.inv_submatrix_equiv @@ -714,4 +715,3 @@ theorem det_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : end Det end Matrix - From ef43d768cf0d26762f3a474099ff791f92f63f10 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 25 Apr 2023 14:12:43 +0200 Subject: [PATCH 5/8] Fixes --- Mathlib/Algebra/Invertible.lean | 3 ++- .../Matrix/NonsingularInverse.lean | 20 ++++++++++--------- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Invertible.lean b/Mathlib/Algebra/Invertible.lean index ff3a80edacc3b..9d648265bbd52 100644 --- a/Mathlib/Algebra/Invertible.lean +++ b/Mathlib/Algebra/Invertible.lean @@ -161,10 +161,11 @@ theorem invertible_unique {α : Type u} [Monoid α] (a b : α) [Invertible a] [I rw [h, mul_invOf_self] #align invertible_unique invertible_unique -instance [Monoid α] (a : α) : Subsingleton (Invertible a) := +instance Invertible.subsingleton [Monoid α] (a : α) : Subsingleton (Invertible a) := ⟨fun ⟨b, hba, hab⟩ ⟨c, _, hac⟩ => by congr exact left_inv_eq_right_inv hba hac⟩ +#align invertible.subsingleton Invertible.subsingleton /-- If `r` is invertible and `s = r`, then `s` is invertible. -/ def Invertible.copy [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (hs : s = r) : diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 7f249bc98e6ee..930094b5dfc7c 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -190,7 +190,7 @@ def invertibleOfInvertibleTranspose [Invertible Aᵀ] : Invertible A := by /-- A matrix is invertible if the conjugate transpose is invertible. -/ def invertibleOfInvertibleConjTranspose [StarRing α] [Invertible Aᴴ] : Invertible A := by - rw [← conjTranspose_conjTranspose A] + rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose] infer_instance #align matrix.invertible_of_invertible_conj_transpose Matrix.invertibleOfInvertibleConjTranspose @@ -528,7 +528,7 @@ def diagonalInvertible {α} [NonAssocSemiring α] (v : n → α) [Invertible v] theorem invOf_diagonal_eq {α} [Semiring α] (v : n → α) [Invertible v] [Invertible (diagonal v)] : ⅟ (diagonal v) = diagonal (⅟ v) := by letI := diagonalInvertible v - haveI := Invertible.subsingleton (diagonal v) + -- Porting note: no longer need `haveI := Invertible.subsingleton (diagonal v)` convert(rfl : ⅟ (diagonal v) = _) #align matrix.inv_of_diagonal_eq Matrix.invOf_diagonal_eq @@ -565,7 +565,7 @@ def diagonalInvertibleEquivInvertible (v : n → α) : Invertible (diagonal v) @[simp] theorem isUnit_diagonal {v : n → α} : IsUnit (diagonal v) ↔ IsUnit v := by simp only [← nonempty_invertible_iff_isUnit, - (diagonal_invertible_equiv_invertible v).nonempty_congr] + (diagonalInvertibleEquivInvertible v).nonempty_congr] #align matrix.is_unit_diagonal Matrix.isUnit_diagonal theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse v) := by @@ -574,7 +574,7 @@ theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse · have := isUnit_diagonal.mpr h cases this.nonempty_invertible cases h.nonempty_invertible - rw [Ring.inverse_invertible, Ring.inverse_invertible, inv_of_diagonal_eq] + rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq] · have := isUnit_diagonal.not.mpr h rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this] #align matrix.inv_diagonal Matrix.inv_diagonal @@ -596,26 +596,28 @@ theorem mul_inv_rev (A B : Matrix n n α) : (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹ : /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /-- A version of `list.prod_inv_reverse` for `matrix.has_inv`. -/ -theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.Prod⁻¹ = (l.reverse.map Inv.inv).Prod +theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.reverse.map Inv.inv).prod | [] => by rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one] | A::Xs => by rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons, Matrix.mul_eq_mul, - Matrix.mul_eq_mul, mul_inv_rev, list_prod_inv_reverse] + Matrix.mul_eq_mul, mul_inv_rev, list_prod_inv_reverse Xs] #align matrix.list_prod_inv_reverse Matrix.list_prod_inv_reverse +set_option synthInstance.etaExperiment true in /-- One form of **Cramer's rule**. See `matrix.mul_vec_cramer` for a stronger form. -/ @[simp] theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • A⁻¹.mulVec b = cramer A b := by - rw [cramer_eq_adjugate_mul_vec, A.nonsing_inv_apply h, ← smul_mul_vec_assoc, smul_smul, - h.mul_coe_inv, one_smul] + rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec_assoc, smul_smul, + h.mul_val_inv, one_smul] #align matrix.det_smul_inv_mul_vec_eq_cramer Matrix.det_smul_inv_mulVec_eq_cramer +set_option synthInstance.etaExperiment true in /-- One form of **Cramer's rule**. See `matrix.mul_vec_cramer` for a stronger form. -/ @[simp] theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • A⁻¹.vecMul b = cramer Aᵀ b := by - rw [← A⁻¹.transpose_transpose, vec_mul_transpose, transpose_nonsing_inv, ← det_transpose, + rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose, Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)] #align matrix.det_smul_inv_vec_mul_eq_cramer_transpose Matrix.det_smul_inv_vecMul_eq_cramer_transpose From 8dd775df0aaf3f7faa90b9ea5166bf89aae498d5 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 25 Apr 2023 14:45:29 +0200 Subject: [PATCH 6/8] Fixes --- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 930094b5dfc7c..9c3f29780974a 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -646,16 +646,18 @@ def invertibleOfSubmatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ [Invertible (A.submatrix e₁ e₂)] : Invertible A := invertibleOfRightInverse _ ((⅟ (A.submatrix e₁ e₂)).submatrix e₂.symm e₁.symm) <| by have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by simp - conv in _ ⬝ _ => - congr - rw [this] + -- Porting note: was + -- conv in _ ⬝ _ => + -- congr + -- rw [this] + rw [congr_arg₂ (· ⬝ ·) this rfl] rw [Matrix.submatrix_mul_equiv, Matrix.mul_invOf_self, submatrix_one_equiv] #align matrix.invertible_of_submatrix_equiv_invertible Matrix.invertibleOfSubmatrixEquivInvertible theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] [Invertible (A.submatrix e₁ e₂)] : ⅟ (A.submatrix e₁ e₂) = (⅟ A).submatrix e₂ e₁ := by letI := submatrixEquivInvertible A e₁ e₂ - haveI := Invertible.subsingleton (A.submatrix e₁ e₂) + -- Porting note: no longer need `haveI := Invertible.subsingleton (A.submatrix e₁ e₂)` convert(rfl : ⅟ (A.submatrix e₁ e₂) = _) #align matrix.inv_of_submatrix_equiv_eq Matrix.invOf_submatrix_equiv_eq @@ -685,7 +687,7 @@ theorem inv_submatrix_equiv (A : Matrix m m α) (e₁ e₂ : n ≃ m) : by_cases h : IsUnit A · cases h.nonempty_invertible letI := submatrixEquivInvertible A e₁ e₂ - rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq] + rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A] · have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h simp_rw [nonsing_inv_eq_ring_inverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this, submatrix_zero, Pi.zero_apply] From 32c65b772974dc5e886ad90d66347e09f6224665 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 25 Apr 2023 17:00:57 +0200 Subject: [PATCH 7/8] Automated --- .../Matrix/NonsingularInverse.lean | 70 +++++++++---------- 1 file changed, 35 insertions(+), 35 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 9c3f29780974a..bc889b80da6ae 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -25,21 +25,21 @@ will result in a multiplicative inverse to `A`. Note that there are at least three different inverses in mathlib: * `A⁻¹` (`has_inv.inv`): alone, this satisfies no properties, although it is usually used in - conjunction with `group` or `group_with_zero`. On matrices, this is defined to be zero when no + conjunction with `Group` or `GroupWithZero`. On matrices, this is defined to be zero when no inverse exists. -* `⅟A` (`inv_of`): this is only available in the presence of `[invertible A]`, which guarantees an +* `⅟A` (`inv_of`): this is only available in the presence of `[Invertible A]`, which guarantees an inverse exists. -* `ring.inverse A`: this is defined on any `monoid_with_zero`, and just like `⁻¹` on matrices, is +* `Ring.inverse A`: this is defined on any `MonoidWithZero`, and just like `⁻¹` on matrices, is defined to be zero when no inverse exists. -We start by working with `invertible`, and show the main results: +We start by working with `Invertible`, and show the main results: -* `matrix.invertible_of_det_invertible` -* `matrix.det_invertible_of_invertible` -* `matrix.is_unit_iff_is_unit_det` -* `matrix.mul_eq_one_comm` +* `Matrix.invertibleOfDetInvertible` +* `Matrix.detInvertibleOfInvertible` +* `Matrix.isUnit_iff_isUnit_det` +* `Matrix.mul_eq_one_comm` -After this we define `matrix.has_inv` and show it matches `⅟A` and `ring.inverse A`. +After this we define `matrix.has_inv` and show it matches `⅟A` and `Ring.inverse A`. The rest of the results in the file are then about `A⁻¹` ## References @@ -62,39 +62,39 @@ open Matrix BigOperators open Equiv Equiv.Perm Finset -/-! ### Matrices are `invertible` iff their determinants are -/ +/-! ### Matrices are `Invertible` iff their determinants are -/ section Invertible variable [Fintype n] [DecidableEq n] [CommRing α] -/-- A copy of `inv_of_mul_self` using `⬝` not `*`. -/ +/-- A copy of `invOf_mul_self` using `⬝` not `*`. -/ protected theorem invOf_mul_self (A : Matrix n n α) [Invertible A] : ⅟ A ⬝ A = 1 := invOf_mul_self A #align matrix.inv_of_mul_self Matrix.invOf_mul_self -/-- A copy of `mul_inv_of_self` using `⬝` not `*`. -/ +/-- A copy of `mul_invOf_self` using `⬝` not `*`. -/ protected theorem mul_invOf_self (A : Matrix n n α) [Invertible A] : A ⬝ ⅟ A = 1 := mul_invOf_self A #align matrix.mul_inv_of_self Matrix.mul_invOf_self -/-- A copy of `inv_of_mul_self_assoc` using `⬝` not `*`. -/ +/-- A copy of `invOf_mul_self_assoc` using `⬝` not `*`. -/ protected theorem invOf_mul_self_assoc (A : Matrix n n α) (B : Matrix n m α) [Invertible A] : ⅟ A ⬝ (A ⬝ B) = B := by rw [← Matrix.mul_assoc, Matrix.invOf_mul_self, Matrix.one_mul] #align matrix.inv_of_mul_self_assoc Matrix.invOf_mul_self_assoc -/-- A copy of `mul_inv_of_self_assoc` using `⬝` not `*`. -/ +/-- A copy of `mul_invOf_self_assoc` using `⬝` not `*`. -/ protected theorem mul_invOf_self_assoc (A : Matrix n n α) (B : Matrix n m α) [Invertible A] : A ⬝ (⅟ A ⬝ B) = B := by rw [← Matrix.mul_assoc, Matrix.mul_invOf_self, Matrix.one_mul] #align matrix.mul_inv_of_self_assoc Matrix.mul_invOf_self_assoc -/-- A copy of `mul_inv_of_mul_self_cancel` using `⬝` not `*`. -/ +/-- A copy of `mul_invOf_mul_self_cancel` using `⬝` not `*`. -/ protected theorem mul_invOf_mul_self_cancel (A : Matrix m n α) (B : Matrix n n α) [Invertible B] : A ⬝ ⅟ B ⬝ B = A := by rw [Matrix.mul_assoc, Matrix.invOf_mul_self, Matrix.mul_one] #align matrix.mul_inv_of_mul_self_cancel Matrix.mul_invOf_mul_self_cancel -/-- A copy of `mul_mul_inv_of_self_cancel` using `⬝` not `*`. -/ +/-- A copy of `mul_mul_invOf_self_cancel` using `⬝` not `*`. -/ protected theorem mul_mul_invOf_self_cancel (A : Matrix m n α) (B : Matrix n n α) [Invertible B] : A ⬝ B ⬝ ⅟ B = A := by rw [Matrix.mul_assoc, Matrix.mul_invOf_self, Matrix.mul_one] #align matrix.mul_mul_inv_of_self_cancel Matrix.mul_mul_invOf_self_cancel @@ -139,7 +139,7 @@ theorem det_invOf [Invertible A] [Invertible A.det] : (⅟ A).det = ⅟ A.det := convert(rfl : _ = ⅟ A.det) #align matrix.det_inv_of Matrix.det_invOf -/-- Together `matrix.det_invertible_of_invertible` and `matrix.invertible_of_det_invertible` form an +/-- Together `Matrix.detInvertibleOfInvertible` and `Matrix.invertibleOfDetInvertible` form an equivalence, although both sides of the equiv are subsingleton anyway. -/ @[simps] def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det where @@ -194,17 +194,17 @@ def invertibleOfInvertibleConjTranspose [StarRing α] [Invertible Aᴴ] : Invert infer_instance #align matrix.invertible_of_invertible_conj_transpose Matrix.invertibleOfInvertibleConjTranspose -/-- Given a proof that `A.det` has a constructive inverse, lift `A` to `(matrix n n α)ˣ`-/ +/-- Given a proof that `A.det` has a constructive inverse, lift `A` to `(Matrix n n α)ˣ`-/ def unitOfDetInvertible [Invertible A.det] : (Matrix n n α)ˣ := @unitOfInvertible _ _ A (invertibleOfDetInvertible A) #align matrix.unit_of_det_invertible Matrix.unitOfDetInvertible -/-- When lowered to a prop, `matrix.invertible_equiv_det_invertible` forms an `iff`. -/ +/-- When lowered to a prop, `Matrix.invertibleEquivDetInvertible` forms an `iff`. -/ theorem isUnit_iff_isUnit_det : IsUnit A ↔ IsUnit A.det := by simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivDetInvertible A).nonempty_congr] #align matrix.is_unit_iff_is_unit_det Matrix.isUnit_iff_isUnit_det -/-! #### Variants of the statements above with `is_unit`-/ +/-! #### Variants of the statements above with `IsUnit`-/ theorem isUnit_det_of_invertible [Invertible A] : IsUnit A.det := @@ -248,7 +248,7 @@ theorem isUnit_det_transpose (h : IsUnit A.det) : IsUnit Aᵀ.det := by exact h #align matrix.is_unit_det_transpose Matrix.isUnit_det_transpose -/-! ### A noncomputable `has_inv` instance -/ +/-! ### A noncomputable `Inv` instance -/ /-- The inverse of a square matrix, when it is invertible (and zero otherwise).-/ @@ -282,7 +282,7 @@ theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n rw [← invOf_eq_nonsing_inv, invOf_units] #align matrix.coe_units_inv Matrix.coe_units_inv -/-- The nonsingular inverse is the same as the general `ring.inverse`. -/ +/-- The nonsingular inverse is the same as the general `Ring.inverse`. -/ theorem nonsing_inv_eq_ring_inverse : A⁻¹ = Ring.inverse A := by by_cases h_det : IsUnit A.det · cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible @@ -425,8 +425,8 @@ theorem isUnit_nonsing_inv_det_iff {A : Matrix n n α} : IsUnit A⁻¹.det ↔ I rw [Matrix.det_nonsing_inv, isUnit_ring_inverse] #align matrix.is_unit_nonsing_inv_det_iff Matrix.isUnit_nonsing_inv_det_iff --- `is_unit.invertible` lifts the proposition `is_unit A` to a constructive inverse of `A`. -/-- A version of `matrix.invertible_of_det_invertible` with the inverse defeq to `A⁻¹` that is +-- `IsUnit.invertible` lifts the proposition `IsUnit A` to a constructive inverse of `A`. +/-- A version of `Matrix.invertibleOfDetInvertible` with the inverse defeq to `A⁻¹` that is therefore noncomputable. -/ noncomputable def invertibleOfIsUnitDet (h : IsUnit A.det) : Invertible A := ⟨A⁻¹, nonsing_inv_mul A h, mul_nonsing_inv A h⟩ @@ -551,7 +551,7 @@ def invertibleOfDiagonalInvertible (v : n → α) [Invertible (diagonal v)] : In exact mul_invOf_self _ #align matrix.invertible_of_diagonal_invertible Matrix.invertibleOfDiagonalInvertible -/-- Together `matrix.diagonal_invertible` and `matrix.invertible_of_diagonal_invertible` form an +/-- Together `Matrix.diagonalInvertible` and `Matrix.invertibleOfDiagonalInvertible` form an equivalence, although both sides of the equiv are subsingleton anyway. -/ @[simps] def diagonalInvertibleEquivInvertible (v : n → α) : Invertible (diagonal v) ≃ Invertible v where @@ -561,7 +561,7 @@ def diagonalInvertibleEquivInvertible (v : n → α) : Invertible (diagonal v) right_inv _ := Subsingleton.elim _ _ #align matrix.diagonal_invertible_equiv_invertible Matrix.diagonalInvertibleEquivInvertible -/-- When lowered to a prop, `matrix.diagonal_invertible_equiv_invertible` forms an `iff`. -/ +/-- When lowered to a prop, `Matrix.diagonalInvertibleEquivInvertible` forms an `iff`. -/ @[simp] theorem isUnit_diagonal {v : n → α} : IsUnit (diagonal v) ↔ IsUnit v := by simp only [← nonempty_invertible_iff_isUnit, @@ -595,7 +595,7 @@ theorem mul_inv_rev (A B : Matrix n n α) : (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹ : #align matrix.mul_inv_rev Matrix.mul_inv_rev /- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/-- A version of `list.prod_inv_reverse` for `matrix.has_inv`. -/ +/-- A version of `List.prod_inv_reverse` for `matrix.has_inv`. -/ theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.reverse.map Inv.inv).prod | [] => by rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one] | A::Xs => by @@ -604,7 +604,7 @@ theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.r #align matrix.list_prod_inv_reverse Matrix.list_prod_inv_reverse set_option synthInstance.etaExperiment true in -/-- One form of **Cramer's rule**. See `matrix.mul_vec_cramer` for a stronger form. -/ +/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ @[simp] theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • A⁻¹.mulVec b = cramer A b := by @@ -613,7 +613,7 @@ theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : Is #align matrix.det_smul_inv_mul_vec_eq_cramer Matrix.det_smul_inv_mulVec_eq_cramer set_option synthInstance.etaExperiment true in -/-- One form of **Cramer's rule**. See `matrix.mul_vec_cramer` for a stronger form. -/ +/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/ @[simp] theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) : A.det • A⁻¹.vecMul b = cramer Aᵀ b := by @@ -623,7 +623,7 @@ theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → /-! ### Inverses of permutated matrices -Note that the simp-normal form of `matrix.reindex` is `matrix.submatrix`, so we prove most of these +Note that the simp-normal form of `Matrix.reindex` is `Matrix.submatrix`, so we prove most of these results about only the latter. -/ @@ -661,8 +661,8 @@ theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Inve convert(rfl : ⅟ (A.submatrix e₁ e₂) = _) #align matrix.inv_of_submatrix_equiv_eq Matrix.invOf_submatrix_equiv_eq -/-- Together `matrix.submatrix_equiv_invertible` and -`matrix.invertible_of_submatrix_equiv_invertible` form an equivalence, although both sides of the +/-- Together `Matrix.submatrixEquivInvertible` and +`Matrix.invertibleOfSubmatrixEquivInvertible` form an equivalence, although both sides of the equiv are subsingleton anyway. -/ @[simps] def submatrixEquivInvertibleEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) : @@ -673,7 +673,7 @@ def submatrixEquivInvertibleEquivInvertible (A : Matrix m m α) (e₁ e₂ : n right_inv _ := Subsingleton.elim _ _ #align matrix.submatrix_equiv_invertible_equiv_invertible Matrix.submatrixEquivInvertibleEquivInvertible -/-- When lowered to a prop, `matrix.invertible_of_submatrix_equiv_invertible` forms an `iff`. -/ +/-- When lowered to a prop, `Matrix.invertibleOfSubmatrixEquivInvertible` forms an `iff`. -/ @[simp] theorem isUnit_submatrix_equiv {A : Matrix m m α} (e₁ e₂ : n ≃ m) : IsUnit (A.submatrix e₁ e₂) ↔ IsUnit A := by @@ -706,12 +706,12 @@ section Det variable [Fintype m] [DecidableEq m] -/-- A variant of `matrix.det_units_conj`. -/ +/-- A variant of `Matrix.det_units_conj`. -/ theorem det_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : det (M ⬝ N ⬝ M⁻¹) = det N := by rw [← h.unit_spec, ← coe_units_inv, det_units_conj] #align matrix.det_conj Matrix.det_conj -/-- A variant of `matrix.det_units_conj'`. -/ +/-- A variant of `Matrix.det_units_conj'`. -/ theorem det_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : det (M⁻¹ ⬝ N ⬝ M) = det N := by rw [← h.unit_spec, ← coe_units_inv, det_units_conj'] #align matrix.det_conj' Matrix.det_conj' From 97f465a50b080ca5a5edc39a906029655d4b8bed Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Tue, 25 Apr 2023 17:16:25 +0200 Subject: [PATCH 8/8] Tidy --- Mathlib/Algebra/Group/Units.lean | 4 +-- .../Matrix/NonsingularInverse.lean | 27 +++++++++---------- 2 files changed, 14 insertions(+), 17 deletions(-) diff --git a/Mathlib/Algebra/Group/Units.lean b/Mathlib/Algebra/Group/Units.lean index 143c7b2e4c705..ca4145f3ddbd2 100644 --- a/Mathlib/Algebra/Group/Units.lean +++ b/Mathlib/Algebra/Group/Units.lean @@ -114,9 +114,9 @@ attribute [instance] AddUnits.instCoeHeadAddUnits /-- The inverse of a unit in a `Monoid`. -/ @[to_additive "The additive inverse of an additive unit in an `AddMonoid`."] -instance : Inv αˣ := +instance instInv : Inv αˣ := ⟨fun u => ⟨u.2, u.1, u.4, u.3⟩⟩ -attribute [instance] AddUnits.instNegAddUnits +attribute [instance] AddUnits.instNeg /- porting note: the result of these definitions is syntactically equal to `Units.val` and `Units.inv` because of the way coercions work in Lean 4, so there is no need for these custom diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index bc889b80da6ae..b71e44062b24a 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -24,10 +24,10 @@ will result in a multiplicative inverse to `A`. Note that there are at least three different inverses in mathlib: -* `A⁻¹` (`has_inv.inv`): alone, this satisfies no properties, although it is usually used in +* `A⁻¹` (`Inv.inv`): alone, this satisfies no properties, although it is usually used in conjunction with `Group` or `GroupWithZero`. On matrices, this is defined to be zero when no inverse exists. -* `⅟A` (`inv_of`): this is only available in the presence of `[Invertible A]`, which guarantees an +* `⅟A` (`invOf`): this is only available in the presence of `[Invertible A]`, which guarantees an inverse exists. * `Ring.inverse A`: this is defined on any `MonoidWithZero`, and just like `⁻¹` on matrices, is defined to be zero when no inverse exists. @@ -39,7 +39,7 @@ We start by working with `Invertible`, and show the main results: * `Matrix.isUnit_iff_isUnit_det` * `Matrix.mul_eq_one_comm` -After this we define `matrix.has_inv` and show it matches `⅟A` and `Ring.inverse A`. +After this we define `Matrix.inv` and show it matches `⅟A` and `Ring.inverse A`. The rest of the results in the file are then about `A⁻¹` ## References @@ -58,9 +58,7 @@ universe u u' v variable {l : Type _} {m : Type u} {n : Type u'} {α : Type v} -open Matrix BigOperators - -open Equiv Equiv.Perm Finset +open Matrix BigOperators Equiv Equiv.Perm Finset /-! ### Matrices are `Invertible` iff their determinants are -/ @@ -267,14 +265,14 @@ theorem nonsing_inv_apply (h : IsUnit A.det) : A⁻¹ = (↑h.unit⁻¹ : α) rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec] #align matrix.nonsing_inv_apply Matrix.nonsing_inv_apply -/-- The nonsingular inverse is the same as `inv_of` when `A` is invertible. -/ +/-- The nonsingular inverse is the same as `invOf` when `A` is invertible. -/ @[simp] theorem invOf_eq_nonsing_inv [Invertible A] : ⅟ A = A⁻¹ := by letI := detInvertibleOfInvertible A rw [inv_def, Ring.inverse_invertible, invOf_eq] #align matrix.inv_of_eq_nonsing_inv Matrix.invOf_eq_nonsing_inv -/-- Coercing the result of `units.has_inv` is the same as coercing first and applying the +/-- Coercing the result of `Units.instInv` is the same as coercing first and applying the nonsingular inverse. -/ @[simp, norm_cast] theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α) := by @@ -376,14 +374,14 @@ theorem inv_mul_cancel_left_of_invertible (B : Matrix n m α) [Invertible A] : A theorem inv_mul_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] : A⁻¹ ⬝ B = C ↔ B = A ⬝ C := - ⟨fun h => by rw [← h, mul_inv_cancel_left_of_invertible], fun h => by - rw [h, inv_mul_cancel_left_of_invertible]⟩ + ⟨fun h => by rw [← h, mul_inv_cancel_left_of_invertible], + fun h => by rw [h, inv_mul_cancel_left_of_invertible]⟩ #align matrix.inv_mul_eq_iff_eq_mul_of_invertible Matrix.inv_mul_eq_iff_eq_mul_of_invertible theorem mul_inv_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] : B ⬝ A⁻¹ = C ↔ B = C ⬝ A := - ⟨fun h => by rw [← h, inv_mul_cancel_right_of_invertible], fun h => by - rw [h, mul_inv_cancel_right_of_invertible]⟩ + ⟨fun h => by rw [← h, inv_mul_cancel_right_of_invertible], + fun h => by rw [h, mul_inv_cancel_right_of_invertible]⟩ #align matrix.mul_inv_eq_iff_eq_mul_of_invertible Matrix.mul_inv_eq_iff_eq_mul_of_invertible theorem nonsing_inv_cancel_or_zero : A⁻¹ ⬝ A = 1 ∧ A ⬝ A⁻¹ = 1 ∨ A⁻¹ = 0 := by @@ -432,7 +430,7 @@ noncomputable def invertibleOfIsUnitDet (h : IsUnit A.det) : Invertible A := ⟨A⁻¹, nonsing_inv_mul A h, mul_nonsing_inv A h⟩ #align matrix.invertible_of_is_unit_det Matrix.invertibleOfIsUnitDet -/-- A version of `matrix.units_of_det_invertible` with the inverse defeq to `A⁻¹` that is therefore +/-- A version of `Matrix.unitOfDetInvertible` with the inverse defeq to `A⁻¹` that is therefore noncomputable. -/ noncomputable def nonsingInvUnit (h : IsUnit A.det) : (Matrix n n α)ˣ := @unitOfInvertible _ _ _ (invertibleOfIsUnitDet A h) @@ -594,8 +592,7 @@ theorem mul_inv_rev (A B : Matrix n n α) : (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹ : Ring.mul_inverse_rev] #align matrix.mul_inv_rev Matrix.mul_inv_rev -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/-- A version of `List.prod_inv_reverse` for `matrix.has_inv`. -/ +/-- A version of `List.prod_inv_reverse` for `Matrix.inv`. -/ theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.reverse.map Inv.inv).prod | [] => by rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one] | A::Xs => by