[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible (det A)
⊢ ⅟(det A) • adjugate A * A = 1
[PROOFSTEP]
rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible (det A)
⊢ A * ⅟(det A) • adjugate A = 1
[PROOFSTEP]
rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Invertible (det A)
inst✝ : Invertible A
⊢ ⅟A = ⅟(det A) • adjugate A
[PROOFSTEP]
letI := invertibleOfDetInvertible A
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Invertible (det A)
inst✝ : Invertible A
this : Invertible A := invertibleOfDetInvertible A
⊢ ⅟A = ⅟(det A) • adjugate A
[PROOFSTEP]
convert (rfl : ⅟A = _)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : B * A = 1
⊢ det B * det A = 1
[PROOFSTEP]
rw [← det_mul, h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : B * A = 1
⊢ det A * det B = 1
[PROOFSTEP]
rw [mul_comm, ← det_mul, h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A * B = 1
⊢ det B * det A = 1
[PROOFSTEP]
rw [mul_comm, ← det_mul, h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A * B = 1
⊢ det A * det B = 1
[PROOFSTEP]
rw [← det_mul, h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (det A)
⊢ det ⅟A = ⅟(det A)
[PROOFSTEP]
letI := detInvertibleOfInvertible A
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible (det A)
this : Invertible (det A) := detInvertibleOfInvertible A
⊢ det ⅟A = ⅟(det A)
[PROOFSTEP]
convert (rfl : _ = ⅟A.det)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
⊢ B * A = 1
[PROOFSTEP]
letI : Invertible B.det := detInvertibleOfLeftInverse _ _ h
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this : Invertible (det B) := detInvertibleOfLeftInverse B A h
⊢ B * A = 1
[PROOFSTEP]
letI : Invertible B := invertibleOfDetInvertible B
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B * A = 1
[PROOFSTEP]
calc
  B * A = B * A * (B * ⅟B) := by rw [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 := mul_invOf_self B
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B * A = B * A * (B * ⅟B)
[PROOFSTEP]
rw [mul_invOf_self, Matrix.mul_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B * A * (B * ⅟B) = B * (A * B * ⅟B)
[PROOFSTEP]
simp only [Matrix.mul_assoc]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
h : A * B = 1
this✝ : Invertible (det B) := detInvertibleOfLeftInverse B A h
this : Invertible B := invertibleOfDetInvertible B
⊢ B * (A * B * ⅟B) = B * ⅟B
[PROOFSTEP]
rw [h, Matrix.one_mul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ Invertible (det Aᵀ)
[PROOFSTEP]
simpa using detInvertibleOfInvertible A
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ Invertible A
[PROOFSTEP]
rw [← transpose_transpose A]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ Invertible Aᵀᵀ
[PROOFSTEP]
infer_instance
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : StarRing α
inst✝ : Invertible Aᴴ
⊢ Invertible A
[PROOFSTEP]
rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : StarRing α
inst✝ : Invertible Aᴴ
⊢ Invertible (star Aᴴ)
[PROOFSTEP]
infer_instance
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ IsUnit A ↔ IsUnit (det A)
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivDetInvertible A).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ IsUnit (det Aᵀ)
[PROOFSTEP]
rw [det_transpose]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ IsUnit (det A)
[PROOFSTEP]
exact h
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
⊢ A⁻¹ = 0
[PROOFSTEP]
rw [inv_def, Ring.inverse_non_unit _ h, zero_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹ = ↑(IsUnit.unit h)⁻¹ • adjugate A
[PROOFSTEP]
rw [inv_def, ← Ring.inverse_unit h.unit, IsUnit.unit_spec]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ ⅟A = A⁻¹
[PROOFSTEP]
letI := detInvertibleOfInvertible A
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
this : Invertible (det A) := detInvertibleOfInvertible A
⊢ ⅟A = A⁻¹
[PROOFSTEP]
rw [inv_def, Ring.inverse_invertible, invOf_eq]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B : Matrix n n α
A : (Matrix n n α)ˣ
⊢ ↑A⁻¹ = (↑A)⁻¹
[PROOFSTEP]
letI := A.invertible
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B : Matrix n n α
A : (Matrix n n α)ˣ
this : Invertible ↑A := Units.invertible A
⊢ ↑A⁻¹ = (↑A)⁻¹
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, invOf_units]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
by_cases h_det : IsUnit A.det
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : IsUnit (det A)
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : IsUnit (det A)
val✝ : Invertible A
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : ¬IsUnit (det A)
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
have h := mt A.isUnit_iff_isUnit_det.mp h_det
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h_det : ¬IsUnit (det A)
h : ¬IsUnit A
⊢ A⁻¹ = Ring.inverse A
[PROOFSTEP]
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ A⁻¹ᵀ = Aᵀ⁻¹
[PROOFSTEP]
rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : StarRing α
⊢ A⁻¹ᴴ = Aᴴ⁻¹
[PROOFSTEP]
rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose, Ring.inverse_star]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A * A⁻¹ = 1
[PROOFSTEP]
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
[GOAL]
case intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible A
⊢ A * A⁻¹ = 1
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, mul_invOf_self]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹ * A = 1
[PROOFSTEP]
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
[GOAL]
case intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible A
⊢ A⁻¹ * A = 1
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, invOf_mul_self]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ Invertible A⁻¹
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ Invertible ⅟A
[PROOFSTEP]
infer_instance
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
⊢ A⁻¹⁻¹ = A
[PROOFSTEP]
simp only [← invOf_eq_nonsing_inv, invOf_invOf]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B✝ : Matrix n n α
B : Matrix m n α
h : IsUnit (det A)
⊢ B * A * A⁻¹ = B
[PROOFSTEP]
simp [Matrix.mul_assoc, mul_nonsing_inv A h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B✝ : Matrix n n α
B : Matrix n m α
h : IsUnit (det A)
⊢ A * (A⁻¹ * B) = B
[PROOFSTEP]
simp [← Matrix.mul_assoc, mul_nonsing_inv A h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B✝ : Matrix n n α
B : Matrix m n α
h : IsUnit (det A)
⊢ B * A⁻¹ * A = B
[PROOFSTEP]
simp [Matrix.mul_assoc, nonsing_inv_mul A h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B✝ : Matrix n n α
B : Matrix n m α
h : IsUnit (det A)
⊢ A⁻¹ * (A * B) = B
[PROOFSTEP]
simp [← Matrix.mul_assoc, nonsing_inv_mul A h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : A⁻¹ * B = C
⊢ B = A * C
[PROOFSTEP]
rw [← h, mul_inv_cancel_left_of_invertible]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : B = A * C
⊢ A⁻¹ * B = C
[PROOFSTEP]
rw [h, inv_mul_cancel_left_of_invertible]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : B * A⁻¹ = C
⊢ B = C * A
[PROOFSTEP]
rw [← h, inv_mul_cancel_right_of_invertible]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A✝ B✝ A B C : Matrix n n α
inst✝ : Invertible A
h : B = C * A
⊢ B * A⁻¹ = C
[PROOFSTEP]
rw [h, mul_inv_cancel_right_of_invertible]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
x✝¹ x✝ : Matrix n m α
h : (fun x => A * x) x✝¹ = (fun x => A * x) x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
simpa only [inv_mul_cancel_left_of_invertible] using congr_arg (A⁻¹ * ·) h
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible A
a x : Matrix m n α
hax : (fun x => x * A) a = (fun x => x * A) x
⊢ a = x
[PROOFSTEP]
simpa only [mul_inv_cancel_right_of_invertible] using congr_arg (· * A⁻¹) hax
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
[PROOFSTEP]
by_cases h : IsUnit A.det
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
[PROOFSTEP]
exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
[PROOFSTEP]
exact Or.inr (nonsing_inv_apply_not_isUnit _ h)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ det A⁻¹ * det A = 1
[PROOFSTEP]
rw [← det_mul, A.nonsing_inv_mul h, det_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
by_cases h : IsUnit A.det
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
cases h.nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible (det A)
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
letI := invertibleOfDetInvertible A
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
val✝ : Invertible (det A)
this : Invertible A := invertibleOfDetInvertible A
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
cases isEmpty_or_nonempty n
[GOAL]
case neg.inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
h✝ : IsEmpty n
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
rw [det_isEmpty, det_isEmpty, Ring.inverse_one]
[GOAL]
case neg.inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : ¬IsUnit (det A)
h✝ : Nonempty n
⊢ det A⁻¹ = Ring.inverse (det A)
[PROOFSTEP]
rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹⁻¹ = 1 * A⁻¹⁻¹
[PROOFSTEP]
rw [Matrix.one_mul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ 1 * A⁻¹⁻¹ = A * A⁻¹ * A⁻¹⁻¹
[PROOFSTEP]
rw [A.mul_nonsing_inv h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit (det A)
⊢ A * A⁻¹ * A⁻¹⁻¹ = A
[PROOFSTEP]
rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
⊢ IsUnit (det A⁻¹) ↔ IsUnit (det A)
[PROOFSTEP]
rw [Matrix.det_nonsing_inv, isUnit_ring_inverse]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible (det A)
⊢ unitOfDetInvertible A = nonsingInvUnit A (_ : IsUnit (det A))
[PROOFSTEP]
ext
[GOAL]
case a.a.h
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
inst✝ : Invertible (det A)
i✝ x✝ : n
⊢ ↑(unitOfDetInvertible A) i✝ x✝ = ↑(nonsingInvUnit A (_ : IsUnit (det A))) i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : B * A = 1
g : C * A = 1
⊢ B = C
[PROOFSTEP]
rw [← inv_eq_left_inv h, ← inv_eq_left_inv g]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : A * C = 1
⊢ B = C
[PROOFSTEP]
rw [← inv_eq_right_inv h, ← inv_eq_right_inv g]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A * B = 1
g : C * A = 1
⊢ B = C
[PROOFSTEP]
rw [← inv_eq_right_inv h, ← inv_eq_left_inv g]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit (det A)
⊢ A = B
[PROOFSTEP]
refine' left_inv_eq_left_inv (mul_nonsing_inv _ h') _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit (det A)
⊢ B * A⁻¹ = 1
[PROOFSTEP]
rw [h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit (det A)
⊢ B * B⁻¹ = 1
[PROOFSTEP]
refine' mul_nonsing_inv _ _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B C : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit (det A)
⊢ IsUnit (det B)
[PROOFSTEP]
rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ 0⁻¹ = 0
[PROOFSTEP]
cases' subsingleton_or_nontrivial α with ht ht
[GOAL]
case inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Subsingleton α
⊢ 0⁻¹ = 0
[PROOFSTEP]
simp
[GOAL]
case inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
⊢ 0⁻¹ = 0
[PROOFSTEP]
cases' (Fintype.card n).zero_le.eq_or_lt with hc hc
[GOAL]
case inr.inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : 0 = Fintype.card n
⊢ 0⁻¹ = 0
[PROOFSTEP]
rw [eq_comm, Fintype.card_eq_zero_iff] at hc 
[GOAL]
case inr.inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : IsEmpty n
⊢ 0⁻¹ = 0
[PROOFSTEP]
haveI := hc
[GOAL]
case inr.inl
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc this : IsEmpty n
⊢ 0⁻¹ = 0
[PROOFSTEP]
ext i
[GOAL]
case inr.inl.a.h
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc this : IsEmpty n
i x✝ : n
⊢ 0⁻¹ i x✝ = OfNat.ofNat 0 i x✝
[PROOFSTEP]
exact (IsEmpty.false i).elim
[GOAL]
case inr.inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : 0 < Fintype.card n
⊢ 0⁻¹ = 0
[PROOFSTEP]
have hn : Nonempty n := Fintype.card_pos_iff.mp hc
[GOAL]
case inr.inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ 0⁻¹ = 0
[PROOFSTEP]
refine' nonsing_inv_apply_not_isUnit _ _
[GOAL]
case inr.inr
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
ht : Nontrivial α
hc : 0 < Fintype.card n
hn : Nonempty n
⊢ ¬IsUnit (det 0)
[PROOFSTEP]
simp [hn]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
src✝¹ : One (Matrix n n α) := one
src✝ : Inv (Matrix n n α) := inv
⊢ 1 * 1 = 1
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
k : α
inst✝ : Invertible k
h : IsUnit (det A)
⊢ ⅟k • A⁻¹ * k • A = 1
[PROOFSTEP]
simp [h, smul_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
k : αˣ
h : IsUnit (det A)
⊢ k⁻¹ • A⁻¹ * k • A = 1
[PROOFSTEP]
simp [h, smul_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : IsUnit (det A)
⊢ (adjugate A)⁻¹ = (IsUnit.unit h)⁻¹ • A
[PROOFSTEP]
refine' inv_eq_left_inv _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : IsUnit (det A)
⊢ (IsUnit.unit h)⁻¹ • A * adjugate A = 1
[PROOFSTEP]
rw [smul_mul, mul_adjugate, Units.smul_def, smul_smul, h.val_inv_mul, one_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α✝ : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α✝
A B : Matrix n n α✝
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
⊢ ⅟(diagonal v) = diagonal ⅟v
[PROOFSTEP]
letI := diagonalInvertible v
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α✝ : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α✝
A B : Matrix n n α✝
α : Type u_2
inst✝² : Semiring α
v : n → α
inst✝¹ : Invertible v
inst✝ : Invertible (diagonal v)
this : Invertible (diagonal v) := diagonalInvertible v
⊢ ⅟(diagonal v) = diagonal ⅟v
[PROOFSTEP]
convert (rfl : ⅟(diagonal v) = _)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
⊢ (diag ⅟(diagonal v) * v) i = OfNat.ofNat 1 i
[PROOFSTEP]
letI : Invertible (diagonal v).det := detInvertibleOfInvertible _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ (diag ⅟(diagonal v) * v) i = OfNat.ofNat 1 i
[PROOFSTEP]
rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ ((⅟(det (diagonal v)) • fun i => ∏ j in erase univ i, v j) * v) i = OfNat.ofNat 1 i
[PROOFSTEP]
dsimp
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ (⅟(det (diagonal v)) * ∏ j in erase univ i, v j) * v i = 1
[PROOFSTEP]
rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ ⅟(det (diagonal v)) * det (diagonal fun x => v x) = 1
[PROOFSTEP]
exact mul_invOf_self _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
⊢ (v * diag ⅟(diagonal v)) i = OfNat.ofNat 1 i
[PROOFSTEP]
letI : Invertible (diagonal v).det := detInvertibleOfInvertible _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ (v * diag ⅟(diagonal v)) i = OfNat.ofNat 1 i
[PROOFSTEP]
rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ (v * ⅟(det (diagonal v)) • fun i => ∏ j in erase univ i, v j) i = OfNat.ofNat 1 i
[PROOFSTEP]
dsimp
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ v i * (⅟(det (diagonal v)) * ∏ j in erase univ i, v j) = 1
[PROOFSTEP]
rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B : Matrix n n α
v : n → α
inst✝ : Invertible (diagonal v)
i : n
this : Invertible (det (diagonal v)) := detInvertibleOfInvertible (diagonal v)
⊢ ⅟(det (diagonal v)) * det (diagonal fun x => v x) = 1
[PROOFSTEP]
exact mul_invOf_self _
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
⊢ IsUnit (diagonal v) ↔ IsUnit v
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, (diagonalInvertibleEquivInvertible v).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
⊢ (diagonal v)⁻¹ = diagonal (Ring.inverse v)
[PROOFSTEP]
rw [nonsing_inv_eq_ring_inverse]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
by_cases h : IsUnit v
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : IsUnit v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
have := isUnit_diagonal.mpr h
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
cases this.nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝ : Invertible (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
cases h.nonempty_invertible
[GOAL]
case pos.intro.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : IsUnit v
this : IsUnit (diagonal v)
val✝¹ : Invertible (diagonal v)
val✝ : Invertible v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : ¬IsUnit v
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
have := isUnit_diagonal.not.mpr h
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
⊢ Ring.inverse (diagonal v) = diagonal (Ring.inverse v)
[PROOFSTEP]
rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
[PROOFSTEP]
by_cases h : IsUnit A.det
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : IsUnit (det A)
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
[PROOFSTEP]
rw [nonsing_inv_nonsing_inv _ h]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
h : ¬IsUnit (det A)
⊢ A⁻¹⁻¹⁻¹ = A⁻¹
[PROOFSTEP]
simp [nonsing_inv_apply_not_isUnit _ h]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
⊢ (A * B)⁻¹ = B⁻¹ * A⁻¹
[PROOFSTEP]
simp only [inv_def]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B✝ A B : Matrix n n α
⊢ Ring.inverse (det (A * B)) • adjugate (A * B) = Ring.inverse (det B) • adjugate B * Ring.inverse (det A) • adjugate A
[PROOFSTEP]
rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, det_mul, adjugate_mul_distrib, Ring.mul_inverse_rev]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (List.prod [])⁻¹ = List.prod (List.map Inv.inv (List.reverse []))
[PROOFSTEP]
rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
Xs : List (Matrix n n α)
⊢ (List.prod (A :: Xs))⁻¹ = List.prod (List.map Inv.inv (List.reverse (A :: Xs)))
[PROOFSTEP]
rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons, mul_inv_rev, list_prod_inv_reverse Xs]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
b : n → α
h : IsUnit (det A)
⊢ det A • mulVec A⁻¹ b = ↑(cramer A) b
[PROOFSTEP]
rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec_assoc, smul_smul, h.mul_val_inv, one_smul]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A✝ B A : Matrix n n α
b : n → α
h : IsUnit (det A)
⊢ det A • vecMul b A⁻¹ = ↑(cramer Aᵀ) b
[PROOFSTEP]
rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
  Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible A
⊢ submatrix A ↑e₁ ↑e₂ * submatrix ⅟A ↑e₂ ↑e₁ = 1
[PROOFSTEP]
rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
⊢ A * submatrix ⅟(submatrix A ↑e₁ ↑e₂) ↑e₂.symm ↑e₁.symm = 1
[PROOFSTEP]
have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by
  simp
    -- Porting note: was
        -- conv in _ * _ =>
        --   congr
        --   rw [this]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
⊢ A = submatrix (submatrix A ↑e₁ ↑e₂) ↑e₁.symm ↑e₂.symm
[PROOFSTEP]
simp
  -- Porting note: was
      -- conv in _ * _ =>
      --   congr
      --   rw [this]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
this : A = submatrix (submatrix A ↑e₁ ↑e₂) ↑e₁.symm ↑e₂.symm
⊢ A * submatrix ⅟(submatrix A ↑e₁ ↑e₂) ↑e₂.symm ↑e₁.symm = 1
[PROOFSTEP]
rw [congr_arg₂ (· * ·) this rfl]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing α
A✝ B : Matrix n n α
inst✝² : Fintype m
inst✝¹ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
this : A = submatrix (submatrix A ↑e₁ ↑e₂) ↑e₁.symm ↑e₂.symm
⊢ submatrix (submatrix A ↑e₁ ↑e₂) ↑e₁.symm ↑e₂.symm * submatrix ⅟(submatrix A ↑e₁ ↑e₂) ↑e₂.symm ↑e₁.symm = 1
[PROOFSTEP]
rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
A✝ B : Matrix n n α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
⊢ ⅟(submatrix A ↑e₁ ↑e₂) = submatrix ⅟A ↑e₂ ↑e₁
[PROOFSTEP]
letI := submatrixEquivInvertible A e₁ e₂
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
A✝ B : Matrix n n α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
this : Invertible (submatrix A ↑e₁ ↑e₂) := submatrixEquivInvertible A e₁ e₂
⊢ ⅟(submatrix A ↑e₁ ↑e₂) = submatrix ⅟A ↑e₂ ↑e₁
[PROOFSTEP]
convert (rfl : ⅟(A.submatrix e₁ e₂) = _)
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
⊢ IsUnit (submatrix A ↑e₁ ↑e₂) ↔ IsUnit A
[PROOFSTEP]
simp only [← nonempty_invertible_iff_isUnit, (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
by_cases h : IsUnit A
[GOAL]
case pos
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
cases h.nonempty_invertible
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
letI := submatrixEquivInvertible A e₁ e₂
[GOAL]
case pos.intro
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : IsUnit A
val✝ : Invertible A
this : Invertible (submatrix A ↑e₁ ↑e₂) := submatrixEquivInvertible A e₁ e₂
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h
[GOAL]
case neg
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A✝ B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
h : ¬IsUnit A
this : ¬IsUnit (submatrix A ↑e₁ ↑e₂)
⊢ (submatrix A ↑e₁ ↑e₂)⁻¹ = submatrix A⁻¹ ↑e₂ ↑e₁
[PROOFSTEP]
simp_rw [nonsing_inv_eq_ring_inverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this, submatrix_zero,
  Pi.zero_apply]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ det (M * N * M⁻¹) = det N
[PROOFSTEP]
rw [← h.unit_spec, ← coe_units_inv, det_units_conj]
[GOAL]
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A B : Matrix n n α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ det (M⁻¹ * N * M) = det N
[PROOFSTEP]
rw [← h.unit_spec, ← coe_units_inv, det_units_conj']
