English
A vector v ∈ α^n is invertible if and only if the diagonal matrix diag(v) is invertible; when diag(v) is invertible, its inverse induces an inverse for v given by diag( diag(v)^{-1} ).
Русский
Вектор v ∈ α^n обратим тогда и только тогда, когда диагональная матрица diag(v) обратима; при обратимости diag(v) её обратная порождает обратную для v в виде diag(v)^{-1}.
LaTeX
$$Invertible(diagonal(v)) ⇔ Invertible(v)$$
Lean4
/-- `v` is invertible if `diagonal v` is -/
def invertibleOfDiagonalInvertible (v : n → α) [Invertible (diagonal v)] : Invertible v
where
invOf := diag (⅟(diagonal v))
invOf_mul_self :=
funext fun i => by
letI : Invertible (diagonal v).det := detInvertibleOfInvertible _
rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
dsimp
rw [mul_assoc, prod_erase_mul _ _ (Finset.mem_univ _), ← det_diagonal]
exact mul_invOf_self _
mul_invOf_self :=
funext fun i => by
letI : Invertible (diagonal v).det := detInvertibleOfInvertible _
rw [invOf_eq, diag_smul, adjugate_diagonal, diag_diagonal]
dsimp
rw [mul_left_comm, mul_prod_erase _ _ (Finset.mem_univ _), ← det_diagonal]
exact mul_invOf_self _
