invOf_diagonal_eq — Mathlib

English

If the diagonal matrix diag(v) is invertible, then its inverse is the diagonal matrix diag(v^{-1}); equivalently, the inverse of a diagonal matrix is obtained by inverting each diagonal entry.

Русский

Если диагональная матрица diag(v) обратима, то её обратная — диагональная diag(v^{-1}); эквивалентно, обратная боку диагональной матрицы получается за счёт обращения каждого диагонального элемента.

LaTeX

$$$(\operatorname{diag}(v))^{-1} = \operatorname{diag}(v^{-1})$$$

Lean4

theorem invOf_diagonal_eq {α} [Semiring α] (v : n → α) [Invertible v] [Invertible (diagonal v)] :
    ⅟(diagonal v) = diagonal (⅟v) :=
  by
  rw [@Invertible.congr _ _ _ _ _ (diagonalInvertible v) rfl]
  rfl

Похожие утверждения