refactor(data/matrix/invertible): more results about invertible matri…

…ces (#19204)

Many results about `invertible` apply directly to matrices simply by replacing `*` with `matrix.mul`.

This also adds some missing lemmas about invertibility of products.

src/algebra/invertible.lean

@@ -109,12 +109,19 @@ by { apply inv_of_eq_right_inv, rw [h, mul_inv_of_self], }
 instance [monoid α] (a : α) : subsingleton (invertible a) :=
 ⟨ λ ⟨b, hba, hab⟩ ⟨c, hca, hac⟩, by { congr, exact left_inv_eq_right_inv hba hac } ⟩
 
+/-- If `r` is invertible and `s = r` and `si = ⅟r`, then `s` is invertible with `⅟s = si`. -/
+def invertible.copy' [mul_one_class α] {r : α} (hr : invertible r) (s : α) (si : α)
+  (hs : s = r) (hsi : si = ⅟r) :
+  invertible s :=
+{ inv_of := si,
+  inv_of_mul_self := by rw [hs, hsi, inv_of_mul_self],
+  mul_inv_of_self := by rw [hs, hsi, mul_inv_of_self] }
+
 /-- If `r` is invertible and `s = r`, then `s` is invertible. -/
+@[reducible]
 def invertible.copy [mul_one_class α] {r : α} (hr : invertible r) (s : α) (hs : s = r) :
   invertible s :=
-{ inv_of := ⅟r,
-  inv_of_mul_self := by rw [hs, inv_of_mul_self],
-  mul_inv_of_self := by rw [hs, mul_inv_of_self] }
+hr.copy' _ _ hs rfl
 
 /-- An `invertible` element is a unit. -/
 @[simps]
@@ -196,6 +203,11 @@ def invertible_mul [monoid α] (a b : α) [invertible a] [invertible b] : invert
   ⅟(a * b) = ⅟b * ⅟a :=
 inv_of_eq_right_inv (by simp [←mul_assoc])
 
+/-- A copy of `invertible_mul` for dot notation. -/
+@[reducible] def invertible.mul [monoid α] {a b : α} (ha : invertible a) (hb : invertible b) :
+  invertible (a * b) :=
+invertible_mul _ _
+
 theorem commute.inv_of_right [monoid α] {a b : α} [invertible b] (h : commute a b) :
   commute a (⅟b) :=
 calc a * (⅟b) = (⅟b) * (b * a * (⅟b)) : by simp [mul_assoc]
@@ -220,6 +232,43 @@ lemma nonzero_of_invertible [mul_zero_one_class α] (a : α) [nontrivial α] [in
 @[priority 100] instance invertible.ne_zero [mul_zero_one_class α] [nontrivial α] (a : α)
   [invertible a] : ne_zero a := ⟨nonzero_of_invertible a⟩
 
+section monoid
+variables [monoid α]
+
+/-- This is the `invertible` version of `units.is_unit_units_mul` -/
+@[reducible] def invertible_of_invertible_mul (a b : α) [invertible a] [invertible (a * b)] :
+  invertible b :=
+{ inv_of := ⅟(a * b) * a,
+  inv_of_mul_self := by rw [mul_assoc, inv_of_mul_self],
+  mul_inv_of_self := by rw [←(is_unit_of_invertible a).mul_right_inj, ←mul_assoc, ←mul_assoc,
+    mul_inv_of_self, mul_one, one_mul] }
+
+/-- This is the `invertible` version of `units.is_unit_mul_units` -/
+@[reducible] def invertible_of_mul_invertible (a b : α) [invertible (a * b)] [invertible b] :
+  invertible a :=
+{ inv_of := b * ⅟(a * b),
+  inv_of_mul_self := by rw [←(is_unit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc,
+    inv_of_mul_self, mul_one, one_mul],
+  mul_inv_of_self := by rw [←mul_assoc, mul_inv_of_self] }
+
+/-- `invertible_of_invertible_mul` and `invertible_mul` as an equivalence. -/
+@[simps] def invertible.mul_left {a : α} (ha : invertible a) (b : α) :
+  invertible b ≃ invertible (a * b) :=
+{ to_fun := λ hb, by exactI invertible_mul a b,
+  inv_fun := λ hab, by exactI invertible_of_invertible_mul a _,
+  left_inv := λ hb, subsingleton.elim _ _,
+  right_inv := λ hab, subsingleton.elim _ _, }
+
+/-- `invertible_of_mul_invertible` and `invertible_mul` as an equivalence. -/
+@[simps] def invertible.mul_right (a : α) {b : α} (ha : invertible b) :
+  invertible a ≃ invertible (a * b) :=
+{ to_fun := λ hb, by exactI invertible_mul a b,
+  inv_fun := λ hab, by exactI invertible_of_mul_invertible _ b,
+  left_inv := λ hb, subsingleton.elim _ _,
+  right_inv := λ hab, subsingleton.elim _ _, }
+
+end monoid
+
 section monoid_with_zero
 variable [monoid_with_zero α]
 

src/data/matrix/invertible.lean

@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import algebra.invertible
+import data.matrix.basic
+
+/-! # Extra lemmas about invertible matrices
+
+Many of the `invertible` lemmas are about `*`; this restates them to be about `⬝`.
+
+For lemmas about the matrix inverse in terms of the determinant and adjugate, see `matrix.has_inv`
+in `linear_algebra/matrix/nonsingular_inverse.lean`.
+-/
+
+open_locale matrix
+
+variables {m n : Type*} {α : Type*}
+variables [fintype n] [decidable_eq n] [semiring α]
+
+namespace matrix
+
+/-- A copy of `inv_of_mul_self` using `⬝` not `*`. -/
+protected lemma inv_of_mul_self (A : matrix n n α) [invertible A] : ⅟A ⬝ A = 1 := inv_of_mul_self A
+
+/-- A copy of `mul_inv_of_self` using `⬝` not `*`. -/
+protected lemma mul_inv_of_self (A : matrix n n α) [invertible A] : A ⬝ ⅟A = 1 := mul_inv_of_self A
+
+/-- A copy of `inv_of_mul_self_assoc` using `⬝` not `*`. -/
+protected lemma inv_of_mul_self_assoc (A : matrix n n α) (B : matrix n m α) [invertible A] :
+  ⅟A ⬝ (A ⬝ B) = B :=
+by rw [←matrix.mul_assoc, matrix.inv_of_mul_self, matrix.one_mul]
+
+/-- A copy of `mul_inv_of_self_assoc` using `⬝` not `*`. -/
+protected lemma mul_inv_of_self_assoc (A : matrix n n α) (B : matrix n m α) [invertible A] :
+  A ⬝ (⅟A ⬝ B) = B :=
+by rw [←matrix.mul_assoc, matrix.mul_inv_of_self, matrix.one_mul]
+
+/-- A copy of `mul_inv_of_mul_self_cancel` using `⬝` not `*`. -/
+protected lemma mul_inv_of_mul_self_cancel (A : matrix m n α) (B : matrix n n α)
+  [invertible B] : A ⬝ ⅟B ⬝ B = A :=
+by rw [matrix.mul_assoc, matrix.inv_of_mul_self, matrix.mul_one]
+
+/-- A copy of `mul_mul_inv_of_self_cancel` using `⬝` not `*`. -/
+protected lemma mul_mul_inv_of_self_cancel (A : matrix m n α) (B : matrix n n α)
+  [invertible B] : A ⬝ B ⬝ ⅟B = A :=
+by rw [matrix.mul_assoc, matrix.mul_inv_of_self, matrix.mul_one]
+
+/-- A copy of `invertible_mul` using `⬝` not `*`. -/
+@[reducible] protected def invertible_mul (A B : matrix n n α) [invertible A] [invertible B] :
+  invertible (A ⬝ B) :=
+{ inv_of := ⅟B ⬝ ⅟A, ..invertible_mul _ _ }
+
+/-- A copy of `invertible.mul` using `⬝` not `*`.-/
+@[reducible] def _root_.invertible.matrix_mul {A B : matrix n n α}
+  (ha : invertible A) (hb : invertible B) : invertible (A ⬝ B) :=
+invertible_mul _ _
+
+protected lemma inv_of_mul {A B : matrix n n α} [invertible A] [invertible B] [invertible (A ⬝ B)] :
+  ⅟(A ⬝ B) = ⅟B ⬝ ⅟A := inv_of_mul _ _
+
+/-- A copy of `invertible_of_invertible_mul` using `⬝` not `*`. -/
+@[reducible] protected def invertible_of_invertible_mul (a b : matrix n n α)
+  [invertible a] [invertible (a ⬝ b)] : invertible b :=
+{ inv_of := ⅟(a ⬝ b) ⬝ a,
+  ..invertible_of_invertible_mul a b }
+
+/-- A copy of `invertible_of_mul_invertible` using `⬝` not `*`. -/
+@[reducible] protected def invertible_of_mul_invertible (a b : matrix n n α)
+  [invertible (a ⬝ b)] [invertible b] : invertible a :=
+{ inv_of := b ⬝ ⅟(a ⬝ b),
+  ..invertible_of_mul_invertible a b }
+
+end matrix
+
+/-- A copy of `invertible.mul_left` using `⬝` not `*`. -/
+@[reducible] def invertible.matrix_mul_left
+  {a : matrix n n α} (ha : invertible a) (b : matrix n n α) : invertible b ≃ invertible (a ⬝ b) :=
+{ to_fun := λ hb, by exactI matrix.invertible_mul a b,
+  inv_fun := λ hab, by exactI matrix.invertible_of_invertible_mul a _,
+  left_inv := λ hb, subsingleton.elim _ _,
+  right_inv := λ hab, subsingleton.elim _ _, }
+
+/-- A copy of `invertible.mul_right` using `⬝` not `*`. -/
+@[reducible] def invertible.matrix_mul_right
+  (a : matrix n n α) {b : matrix n n α} (ha : invertible b) : invertible a ≃ invertible (a ⬝ b) :=
+{ to_fun := λ hb, by exactI matrix.invertible_mul a b,
+  inv_fun := λ hab, by exactI matrix.invertible_of_mul_invertible _ b,
+  left_inv := λ hb, subsingleton.elim _ _,
+  right_inv := λ hab, subsingleton.elim _ _, }

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -3,6 +3,7 @@ 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
 -/
+import data.matrix.invertible
 import linear_algebra.matrix.adjugate
 
 /-!
@@ -60,31 +61,6 @@ open equiv equiv.perm finset
 section invertible
 variables [fintype n] [decidable_eq n] [comm_ring α]
 
-/-- A copy of `inv_of_mul_self` using `⬝` not `*`. -/
-protected lemma inv_of_mul_self (A : matrix n n α) [invertible A] : ⅟A ⬝ A = 1 := inv_of_mul_self A
-
-/-- A copy of `mul_inv_of_self` using `⬝` not `*`. -/
-protected lemma mul_inv_of_self (A : matrix n n α) [invertible A] : A ⬝ ⅟A = 1 := mul_inv_of_self A
-
-/-- A copy of `inv_of_mul_self_assoc` using `⬝` not `*`. -/
-protected lemma inv_of_mul_self_assoc (A : matrix n n α) (B : matrix n m α) [invertible A] :
-  ⅟A ⬝ (A ⬝ B) = B :=
-by rw [←matrix.mul_assoc, matrix.inv_of_mul_self, matrix.one_mul]
-
-/-- A copy of `mul_inv_of_self_assoc` using `⬝` not `*`. -/
-protected lemma mul_inv_of_self_assoc (A : matrix n n α) (B : matrix n m α) [invertible A] :
-  A ⬝ (⅟A ⬝ B) = B :=
-by rw [←matrix.mul_assoc, matrix.mul_inv_of_self, matrix.one_mul]
-
-/-- A copy of `mul_inv_of_mul_self_cancel` using `⬝` not `*`. -/
-protected lemma mul_inv_of_mul_self_cancel (A : matrix m n α) (B : matrix n n α)
-  [invertible B] : A ⬝ ⅟B ⬝ B = A :=
-by rw [matrix.mul_assoc, matrix.inv_of_mul_self, matrix.mul_one]
-
-/-- A copy of `mul_mul_inv_of_self_cancel` using `⬝` not `*`. -/
-protected lemma mul_mul_inv_of_self_cancel (A : matrix m n α) (B : matrix n n α)
-  [invertible B] : A ⬝ B ⬝ ⅟B = A :=
-by rw [matrix.mul_assoc, matrix.mul_inv_of_self, matrix.mul_one]
 
 variables (A : matrix n n α) (B : matrix n n α)