no goals
l : Type ?u.338640
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
simp only [← nonempty_invertible_iff_isUnit,
  (diagonalInvertibleEquivInvertible v).nonempty_congr]