l : Type ?u.262717
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
l : Type ?u.262717
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
refine' left_inv_eq_left_inv (mul_nonsing_inv _ h') _
l : Type ?u.262717
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
l : Type ?u.262717
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
rw [h]
l : Type ?u.262717
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)
l : Type ?u.262717
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
refine' mul_nonsing_inv _ _
no goals
l : Type ?u.262717
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)
rwa [← isUnit_nonsing_inv_det_iff, ← h, isUnit_nonsing_inv_det_iff]