diagonalInvertible — Mathlib

English

A diagonal matrix diag(v) is invertible whenever the function v : n → α is invertible componentwise.

Русский

Диагональная матрица diag(v) обратима тогда, когда вектор v является обратимым по каждой компоненте.

LaTeX

$$If v: n → α and v is invertible, then Invertible (diagonal v).$$

Lean4

/-- `diagonal v` is invertible if `v` is -/
def diagonalInvertible {α} [NonAssocSemiring α] (v : n → α) [Invertible v] : Invertible (diagonal v) :=
  Invertible.map (diagonalRingHom n α) v

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