English
For any v, the inverse of the diagonal matrix diag(v) equals the diagonal matrix with entries given by the ring-theoretic inverse of v: (diagonal v)^{-1} = diagonal(Ring.inverse(v)).
Русский
Для любого v обратная диагональной матрицы diag(v) равна диагональной матрице с элементами Ring.inverse(v).
LaTeX
$$(diagonal v)^{-1} = diagonal(Ring.inverse v)$$
Lean4
theorem inv_diagonal (v : n → α) : (diagonal v)⁻¹ = diagonal (Ring.inverse v) :=
by
rw [nonsing_inv_eq_ringInverse]
by_cases h : IsUnit v
· have := isUnit_diagonal.mpr h
cases this.nonempty_invertible
cases h.nonempty_invertible
rw [Ring.inverse_invertible, Ring.inverse_invertible, invOf_diagonal_eq]
· have := isUnit_diagonal.not.mpr h
rw [Ring.inverse_non_unit _ h, Pi.zero_def, diagonal_zero, Ring.inverse_non_unit _ this]
