English
There is a natural equivalence between invertible diagonal matrices and invertible vectors: Invertible (diagonal v) is equivalent to Invertible v, with the forward map taking a diagonal invertible to itself and the backward map recovering the diagonal from invertibility.
Русский
Существует естественное эквивалентное соотношение между обратимыми диагональными матрицами и обратимыми векторами: invertible (diagonal v) эквивалентно invertible v.
LaTeX
$$Invertible(diagonal(v)) ≃ Invertible(v)$$
Lean4
/-- Together `Matrix.diagonalInvertible` and `Matrix.invertibleOfDiagonalInvertible` form an
equivalence, although both sides of the equiv are subsingleton anyway. -/
@[simps]
def diagonalInvertibleEquivInvertible (v : n → α) : Invertible (diagonal v) ≃ Invertible v
where
toFun := @invertibleOfDiagonalInvertible _ _ _ _ _ _
invFun := @diagonalInvertible _ _ _ _ _ _
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _
