chore(linear_algebra/nonsingular_inverse): matrix.nonsing_inv no lo…

…nger requires base ring to carry `has_inv` instance (#3136)

src/algebra/group/units.lean

@@ -82,6 +82,12 @@ attribute [norm_cast] add_units.coe_neg
 @[simp, to_additive] lemma inv_mul : (↑a⁻¹ * a : α) = 1 := inv_val _
 @[simp, to_additive] lemma mul_inv : (a * ↑a⁻¹ : α) = 1 := val_inv _
 
+@[to_additive] lemma inv_mul' {u : units α} {a : α} (h : ↑u = a) : ↑u⁻¹ * a = 1 :=
+by { rw [←h, u.inv_mul], }
+
+@[to_additive] lemma mul_inv' {u : units α} {a : α} (h : ↑u = a) : a * ↑u⁻¹ = 1 :=
+by { rw [←h, u.mul_inv], }
+
 @[simp, to_additive] lemma mul_inv_cancel_left (a : units α) (b : α) : (a:α) * (↑a⁻¹ * b) = b :=
 by rw [← mul_assoc, mul_inv, one_mul]
 
@@ -119,6 +125,14 @@ by rw [mul_assoc, inv_mul, mul_one]
 @[to_additive] theorem mul_inv_eq_iff_eq_mul {a c : α} : a * ↑b⁻¹ = c ↔ a = c * b :=
 ⟨λ h, by rw [← h, inv_mul_cancel_right], λ h, by rw [h, mul_inv_cancel_right]⟩
 
+lemma inv_eq_of_mul_eq_one {u : units α} {a : α} (h : ↑u * a = 1) : ↑u⁻¹ = a :=
+calc ↑u⁻¹ = ↑u⁻¹ * 1 : by rw mul_one
+      ... = ↑u⁻¹ * ↑u * a : by rw [←h, ←mul_assoc]
+      ... = a : by rw [u.inv_mul, one_mul]
+
+lemma inv_unique {u₁ u₂ : units α} (h : (↑u₁ : α) = ↑u₂) : (↑u₁⁻¹ : α) = ↑u₂⁻¹ :=
+suffices ↑u₁ * (↑u₂⁻¹ : α) = 1, by exact inv_eq_of_mul_eq_one this, by rw [h, u₂.mul_inv]
+
 end units
 
 /-- For `a, b` in a `comm_monoid` such that `a * b = 1`, makes a unit out of `a`. -/
@@ -256,4 +270,11 @@ by cases ha with a ha; rw [←ha, units.mul_right_inj]
   b * a = c * a ↔ b = c :=
 by cases ha with a ha; rw [←ha, units.mul_left_inj]
 
+/-- The element of the group of units, corresponding to an element of a monoid which is a unit. -/
+noncomputable def is_unit.unit [monoid M] {a : M} (h : is_unit a) : units M :=
+classical.some h
+
+lemma is_unit.unit_spec [monoid M] {a : M} (h : is_unit a) : ↑h.unit = a :=
+classical.some_spec h
+
 end is_unit

src/algebra/invertible.lean

@@ -73,6 +73,10 @@ by simp [mul_assoc]
 lemma inv_of_eq_right_inv [monoid α] {a b : α} [invertible a] (hac : a * b = 1) : ⅟a = b :=
 left_inv_eq_right_inv (inv_of_mul_self _) hac
 
+lemma invertible_unique {α : Type u} [monoid α] (a b : α) (h : a = b) [invertible a] [invertible b] :
+  ⅟a = ⅟b :=
+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 } ⟩
 

src/linear_algebra/nonsingular_inverse.lean

@@ -354,33 +354,77 @@ Defines the matrix `nonsing_inv A` and proves it is the inverse matrix
 of a square matrix `A` as long as `det A` has a multiplicative inverse.
 -/
 
-variables [comm_ring α] [has_inv α]
+variables [comm_ring α]
+variables (A : matrix n n α)
 
-/-- The inverse of a nonsingular matrix.
+open_locale classical
 
-  This is not the most general possible definition, so we don't instantiate `has_inv` (yet).
--/
-def nonsing_inv (A : matrix n n α) : matrix n n α := (A.det)⁻¹ • adjugate A
+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
 
-lemma nonsing_inv_val (A : matrix n n α) (i j : n) :
-  A.nonsing_inv i j = (A.det)⁻¹ * adjugate A i j := rfl
+noncomputable instance : has_inv (matrix n n α) := ⟨matrix.nonsing_inv⟩
 
-lemma transpose_nonsing_inv (A : matrix n n α) : (A.nonsing_inv)ᵀ = (Aᵀ).nonsing_inv :=
-by {ext, simp [transpose_val, nonsing_inv_val, det_transpose, (adjugate_transpose A).symm]}
+lemma nonsing_inv_apply (h : is_unit A.det) :
+  A⁻¹ = (↑h.unit⁻¹ : α) • A.adjugate :=
+by { change A.nonsing_inv = _, dunfold nonsing_inv, simp only [dif_pos, h], }
+
+lemma transpose_nonsing_inv (h : is_unit A.det) :
+  (A⁻¹)ᵀ = (Aᵀ)⁻¹ :=
+begin
+  have h' := A.is_unit_det_transpose h,
+  have dets_eq : (↑h.unit : α) = ↑h'.unit := by rw [h.unit_spec, h'.unit_spec, det_transpose],
+  rw [A.nonsing_inv_apply h, Aᵀ.nonsing_inv_apply h',
+      units.inv_unique dets_eq, A.adjugate_transpose.symm],
+  refl,
+end
 
 /-- The `nonsing_inv` of `A` is a right inverse. -/
-theorem mul_nonsing_inv (A : matrix n n α) (inv_mul_cancel : A.det⁻¹ * A.det = 1) :
-  A ⬝ nonsing_inv A = 1 :=
-by erw [mul_smul, mul_adjugate, smul_smul, inv_mul_cancel, one_smul]
+@[simp] lemma mul_nonsing_inv (h : is_unit A.det) : A ⬝ A⁻¹ = 1 :=
+by rw [A.nonsing_inv_apply h, mul_smul, mul_adjugate, smul_smul, units.inv_mul' h.unit_spec,
+       one_smul]
 
 /-- The `nonsing_inv` of `A` is a left inverse. -/
-theorem nonsing_inv_mul (A : matrix n n α) (inv_mul_cancel : A.det⁻¹ * A.det = 1) :
-  nonsing_inv A ⬝ A = 1 :=
-have inv_mul_cancel' : (det Aᵀ)⁻¹ * det Aᵀ = 1 := by {rw det_transpose, assumption},
-calc nonsing_inv A ⬝ A
-    = (Aᵀ ⬝ nonsing_inv (Aᵀ))ᵀ : by rw [transpose_mul, transpose_nonsing_inv, transpose_transpose]
-... = 1ᵀ                       : by rw [mul_nonsing_inv Aᵀ inv_mul_cancel']
-... = 1                        : transpose_one
+@[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),
+                                    transpose_transpose], }
+         ... = 1ᵀ             : by { rw Aᵀ.mul_nonsing_inv, exact A.is_unit_det_transpose h, }
+         ... = 1              : transpose_one
+
+@[simp] lemma nonsing_inv_det (h : is_unit A.det) : A⁻¹.det * A.det = 1 :=
+by rw [←det_mul, A.nonsing_inv_mul h, det_one]
+
+lemma is_unit_nonsing_inv_det (h : is_unit A.det) : is_unit A⁻¹.det :=
+is_unit_of_mul_eq_one _ _ (A.nonsing_inv_det h)
+
+@[simp] lemma nonsing_inv_nonsing_inv (h : is_unit 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], }
+
+/-- A matrix whose determinant is a unit is itself a unit. -/
+noncomputable def nonsing_inv_unit (h : is_unit A.det) : units (matrix n n α) :=
+{ val     := A,
+  inv     := A⁻¹,
+  val_inv := by { rw matrix.mul_eq_mul, apply A.mul_nonsing_inv h, },
+  inv_val := by { rw matrix.mul_eq_mul, apply A.nonsing_inv_mul h, } }
+
+lemma is_unit_iff_is_unit_det : is_unit A ↔ is_unit A.det :=
+begin
+  split; intros h,
+  { -- is_unit A → is_unit A.det
+    suffices : ∃ (B : matrix n n α), A ⬝ B = 1,
+    { rcases this with ⟨B, hB⟩, apply is_unit_of_mul_eq_one _ B.det, rw [←det_mul, hB, det_one], },
+    refine ⟨↑h.unit⁻¹, _⟩, conv_lhs { congr, rw ←h.unit_spec, }, exact h.unit.mul_inv, },
+  { -- is_unit A.det → is_unit A
+    exact is_unit_unit (A.nonsing_inv_unit h), },
+end
 
 end inv
 end matrix