case a.a.h
l : Type ?u.255443
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✝
l : Type ?u.255443
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))
ext
no goals
case a.a.h
l : Type ?u.255443
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✝
rfl