isUnit_diagonal — Mathlib

English

The unit-ness of a diagonal matrix diag(v) is equivalent to the unit-ness of the vector v: diag(v) is a unit matrix iff every component v_i is a unit in the base ring.

Русский

Единичность диагональной матрицы diag(v) эквивалентна единичности вектора v: diag(v) единична тогда и только тогда, когда каждая компонента v_i является единицей в кольце-основе.

LaTeX

$$IsUnit(diagonal(v)) ⇔ IsUnit(v)$$

Lean4

/-- When lowered to a prop, `Matrix.diagonalInvertibleEquivInvertible` forms an `iff`. -/
@[simp]
theorem isUnit_diagonal {v : n → α} : IsUnit (diagonal v) ↔ IsUnit v := by
  simp only [← nonempty_invertible_iff_isUnit, (diagonalInvertibleEquivInvertible v).nonempty_congr]

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