refactor(linear_algebra/matrix/nonsingular_inverse): use ring.inverse…

… in matrix.has_inv (#9863)

This makes some of the proofs a little shorter.
Independently, this removes an assumption from `matrix.transpose_nonsing_inv`.

This adds the missing `units.is_unit_units_mul` to complement the existing `units.is_unit_mul_units`, even though it ultimately was not used in this PR.

This removes the def `matrix.nonsing_inv` in favor of just using `has_inv.inv` directly. Having two ways to spell the same thing isn't helpful here.

docs/overview.yaml

@@ -161,7 +161,7 @@ Linear algebra:
     ring-valued matrix: 'matrix'
     matrix representation of a linear map: 'linear_map.to_matrix'
     determinant: 'matrix.det'
-    invertibility: 'matrix.nonsing_inv'
+    invertibility: 'matrix.has_inv'
   Endomorphism polynomials:
     minimal polynomial: 'minpoly'
     characteristic polynomial: 'matrix.charpoly'

docs/undergrad.yaml

@@ -45,7 +45,7 @@ Linear algebra:
     change of basis: 'basis_to_matrix_mul_linear_map_to_matrix_mul_basis_to_matrix'
     rank of a matrix: ''
     determinant: 'matrix.det'
-    invertibility: 'matrix.nonsing_inv'
+    invertibility: 'matrix.has_inv'
     elementary row operations: ''
     elementary column operations: ''
     Gaussian elimination: ''

src/algebra/group/units.lean

@@ -295,20 +295,31 @@ by { rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩, exact ⟨b, hba⟩ }
   {a : M} : is_unit a ↔ ∃ b, b * a = 1 :=
 by simp [is_unit_iff_exists_inv, mul_comm]
 
-/-- Multiplication by a `u : units M` doesn't affect `is_unit`. -/
-@[simp, to_additive is_add_unit_add_add_units "Addition of a `u : add_units M` doesn't affect
-`is_add_unit`."]
+@[to_additive]
+lemma is_unit.mul [monoid M] {x y : M} : is_unit x → is_unit y → is_unit (x * y) :=
+by { rintros ⟨x, rfl⟩ ⟨y, rfl⟩, exact ⟨x * y, units.coe_mul _ _⟩ }
+
+/-- Multiplication by a `u : units M` on the right doesn't affect `is_unit`. -/
+@[simp, to_additive is_add_unit_add_add_units "Addition of a `u : add_units M` on the right doesn't
+affect `is_add_unit`."]
 theorem units.is_unit_mul_units [monoid M] (a : M) (u : units M) :
   is_unit (a * u) ↔ is_unit a :=
 iff.intro
   (assume ⟨v, hv⟩,
     have is_unit (a * ↑u * ↑u⁻¹), by existsi v * u⁻¹; rw [←hv, units.coe_mul],
     by rwa [mul_assoc, units.mul_inv, mul_one] at this)
-  (assume ⟨v, hv⟩, hv ▸ ⟨v * u, (units.coe_mul v u).symm⟩)
+  (λ v, v.mul u.is_unit)
 
-@[to_additive]
-lemma is_unit.mul [monoid M] {x y : M} : is_unit x → is_unit y → is_unit (x * y) :=
-by { rintros ⟨x, rfl⟩ ⟨y, rfl⟩, exact ⟨x * y, units.coe_mul _ _⟩ }
+/-- Multiplication by a `u : units M` on the left doesn't affect `is_unit`. -/
+@[simp, to_additive is_add_unit_add_units_add "Addition of a `u : add_units M` on the left doesn't
+affect `is_add_unit`."]
+theorem units.is_unit_units_mul {M : Type*} [monoid M] (u : units M) (a : M) :
+  is_unit (↑u * a) ↔ is_unit a :=
+iff.intro
+  (assume ⟨v, hv⟩,
+    have is_unit (↑u⁻¹ * (↑u * a)), by existsi u⁻¹ * v; rw [←hv, units.coe_mul],
+    by rwa [←mul_assoc, units.inv_mul, one_mul] at this)
+  u.is_unit.mul
 
 @[to_additive is_add_unit_of_add_is_add_unit_left]
 theorem is_unit_of_mul_is_unit_left [comm_monoid M] {x y : M}

src/algebra/ring/basic.lean

@@ -1074,6 +1074,18 @@ by rw [← mul_assoc, mul_inverse_cancel x h, one_mul]
 lemma inverse_mul_cancel_left (x y : M₀) (h : is_unit x) : inverse x * (x * y) = y :=
 by rw [← mul_assoc, inverse_mul_cancel x h, one_mul]
 
+lemma mul_inverse_rev {M₀ : Type*} [comm_monoid_with_zero M₀] (a b : M₀) :
+  ring.inverse (a * b) = ring.inverse b * ring.inverse a :=
+begin
+  by_cases hab : is_unit (a * b),
+  { obtain ⟨⟨a, rfl⟩, b, rfl⟩ := is_unit.mul_iff.mp hab,
+    rw [←units.coe_mul, ring.inverse_unit, ring.inverse_unit, ring.inverse_unit, ←units.coe_mul,
+      mul_inv_rev], },
+  obtain ha | hb := not_and_distrib.mp (mt is_unit.mul_iff.mpr hab),
+  { rw [ring.inverse_non_unit _ hab, ring.inverse_non_unit _ ha, mul_zero]},
+  { rw [ring.inverse_non_unit _ hab, ring.inverse_non_unit _ hb, zero_mul]},
+end
+
 end ring
 
 namespace semiconj_by

src/linear_algebra/bilinear_form.lean

@@ -1213,7 +1213,7 @@ begin
   suffices : x * ↑u = ↑v * y ↔ ↑v⁻¹ * x = y * ↑u⁻¹,
   { dunfold matrix.is_adjoint_pair,
     repeat { rw matrix.transpose_mul, },
-    simp only [←matrix.mul_eq_mul, ←mul_assoc, P.transpose_nonsing_inv h'],
+    simp only [←matrix.mul_eq_mul, ←mul_assoc, P.transpose_nonsing_inv],
     conv_lhs { to_rhs, rw [mul_assoc, mul_assoc], congr, skip, rw ←mul_assoc, },
     conv_rhs { rw [mul_assoc, mul_assoc], conv { to_lhs, congr, skip, rw ←mul_assoc }, },
     exact this, },

src/linear_algebra/matrix/fpow.lean

@@ -205,9 +205,9 @@ theorem semiconj_by.fpow_right {A X Y : M} (hx : is_unit X.det) (hy : is_unit Y.
       semiconj_by],
   refine (is_regular_of_is_left_regular_det hy'.is_regular.left).left _,
   rw [←mul_assoc, ←(h.pow_right n.succ).eq, mul_assoc, mul_eq_mul (X ^ _), mul_smul, mul_adjugate,
-      mul_eq_mul, mul_eq_mul, mul_eq_mul, ←matrix.mul_assoc, mul_smul (Y ^ _) (hy'.unit)⁻¹,
-      mul_adjugate, units.smul_def, units.smul_def, smul_smul, smul_smul, hx'.coe_inv_mul,
-      hy'.coe_inv_mul, one_smul, matrix.mul_one, matrix.one_mul]
+      mul_eq_mul, mul_eq_mul, mul_eq_mul, ←matrix.mul_assoc, mul_smul (Y ^ _) (↑(hy'.unit)⁻¹ : R),
+      mul_adjugate, smul_smul, smul_smul, hx'.coe_inv_mul,
+      hy'.coe_inv_mul, one_smul, matrix.mul_one, matrix.one_mul],
 end
 
 theorem commute.fpow_right {A B : M} (h : commute A B) (m : ℤ) : commute A (B^m) :=

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -30,7 +30,7 @@ replace the `i`th row of `A` with the `j`th basis vector; this has the same
 determinant as the minor but more importantly equals Cramer's rule applied
 to `A` and the `j`th basis vector, simplifying the subsequent proofs.
 We prove the adjugate behaves like `det A • A⁻¹`. Finally, we show that dividing
-the adjugate by `det A` (if possible), giving a matrix `nonsing_inv A`, will
+the adjugate by `det A` (if possible), giving a matrix `A⁻¹` (`nonsing_inv`), will
 result in a multiplicative inverse to `A`.
 
 ## References
@@ -330,7 +330,7 @@ section inv
 /-!
 ### `inv` section
 
-Defines the matrix `nonsing_inv A` and proves it is the inverse matrix
+Defines the matrix `A⁻¹` and proves it is the inverse matrix
 of a square matrix `A` as long as `det A` has a multiplicative inverse.
 -/
 
@@ -341,40 +341,35 @@ open_locale classical
 lemma is_unit_det_transpose (h : is_unit A.det) : is_unit Aᵀ.det :=
 by { rw det_transpose, exact h, }
 
-/-- The inverse of a square matrix, when it is invertible (and zero otherwise).-/
-noncomputable def nonsing_inv : matrix n n α :=
-if h : is_unit A.det then h.unit⁻¹ • A.adjugate else 0
 
-noncomputable instance : has_inv (matrix n n α) := ⟨matrix.nonsing_inv⟩
+/-- The inverse of a square matrix, when it is invertible (and zero otherwise).-/
+noncomputable instance : has_inv (matrix n n α) := ⟨λ A, ring.inverse A.det • A.adjugate⟩
 
-lemma inv_def (A : matrix n n α) : A⁻¹ = A.nonsing_inv := rfl
+lemma inv_def (A : matrix n n α) : A⁻¹ = ring.inverse A.det • A.adjugate := rfl
 
 lemma nonsing_inv_apply_not_is_unit (h : ¬ is_unit A.det) :
   A⁻¹ = 0 :=
-by rw [inv_def, nonsing_inv, dif_neg h]
+by rw [inv_def, ring.inverse_non_unit _ h, zero_smul]
 
 lemma nonsing_inv_apply (h : is_unit A.det) :
-  A⁻¹ = h.unit⁻¹ • A.adjugate :=
-by rw [inv_def, nonsing_inv, dif_pos h]
-
-lemma transpose_nonsing_inv (h : is_unit A.det) :
-  (A⁻¹)ᵀ = (Aᵀ)⁻¹ :=
+  A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate :=
 begin
-  have h' := A.is_unit_det_transpose h,
-  have dets_eq : h.unit = h'.unit := units.ext (by rw [h.unit_spec, h'.unit_spec, det_transpose]),
-  rw [A.nonsing_inv_apply h, Aᵀ.nonsing_inv_apply h', dets_eq, A.adjugate_transpose.symm],
+  rw [inv_def, ←ring.inverse_unit h.unit],
   refl,
 end
 
+lemma transpose_nonsing_inv : (A⁻¹)ᵀ = (Aᵀ)⁻¹ :=
+by rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]
+
 /-- The `nonsing_inv` of `A` is a right inverse. -/
 @[simp] lemma mul_nonsing_inv (h : is_unit A.det) : A ⬝ A⁻¹ = 1 :=
-by rw [A.nonsing_inv_apply h, units.smul_def, mul_smul, mul_adjugate, smul_smul,
+by rw [A.nonsing_inv_apply h, mul_smul, mul_adjugate, smul_smul,
        units.inv_mul_of_eq h.unit_spec, one_smul]
 
 /-- The `nonsing_inv` of `A` is a left inverse. -/
 @[simp] lemma nonsing_inv_mul (h : is_unit A.det) : A⁻¹ ⬝ A = 1 :=
 calc A⁻¹ ⬝ A = (Aᵀ ⬝ (Aᵀ)⁻¹)ᵀ : by { rw [transpose_mul,
-                                    Aᵀ.transpose_nonsing_inv (A.is_unit_det_transpose h),
+                                    Aᵀ.transpose_nonsing_inv,
                                     transpose_transpose], }
          ... = 1ᵀ             : by { rw Aᵀ.mul_nonsing_inv, exact A.is_unit_det_transpose h, }
          ... = 1              : transpose_one
@@ -609,23 +604,6 @@ begin
   { simp [nonsing_inv_apply_not_is_unit _ h] }
 end
 
-lemma mul_inv_rev (A B : matrix n n α) : (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹ :=
-begin
-  by_cases h : is_unit (A ⬝ B).det,
-  { refine inv_eq_left_inv _,
-    rw det_mul at h,
-    rw [←matrix.mul_assoc, matrix.mul_assoc _ _ A,
-        nonsing_inv_mul _ (is_unit_of_mul_is_unit_left h),
-        matrix.mul_one, nonsing_inv_mul _ (is_unit_of_mul_is_unit_right h)] },
-  { rw nonsing_inv_apply_not_is_unit _ h,
-    rw det_mul at h,
-    have : ¬ is_unit A.det ∨ ¬ is_unit B.det,
-    { contrapose! h,
-      exact h.left.mul h.right },
-    cases this with h' h';
-    simp [nonsing_inv_apply_not_is_unit _ h'] }
-end
-
 lemma ring_hom.map_adjugate {R S : Type*} [comm_ring R] [comm_ring S] (f : R →+* S)
   (M : matrix n n R) : f.map_matrix M.adjugate = matrix.adjugate (f.map_matrix M) :=
 begin
@@ -694,6 +672,13 @@ begin
       ring_hom.map_adjugate, f'_inv, f'_g_mul]
 end
 
+lemma mul_inv_rev (A B : matrix n n α) : (A ⬝ B)⁻¹ = B⁻¹ ⬝ A⁻¹ :=
+begin
+  simp only [inv_def],
+  rw [matrix.smul_mul, matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib,
+    ring.mul_inverse_rev],
+end
+
 @[simp] lemma adjugate_pow (A : matrix n n α) (k : ℕ) :
   adjugate (A ^ k) = (adjugate A) ^ k :=
 begin
@@ -708,7 +693,7 @@ end inv
 @[simp] lemma det_smul_inv_mul_vec_eq_cramer (A : matrix n n α) (b : n → α) (h : is_unit A.det) :
   A.det • A⁻¹.mul_vec b = cramer A b :=
 begin
-  rw [cramer_eq_adjugate_mul_vec, A.nonsing_inv_apply h, ← smul_mul_vec_assoc, units.smul_def,
+  rw [cramer_eq_adjugate_mul_vec, A.nonsing_inv_apply h, ← smul_mul_vec_assoc,
       smul_smul, h.mul_coe_inv, one_smul]
 end