isDiag_of_subsingleton — Mathlib

English

Every matrix indexed by a subsingleton is diagonal.

Русский

Каждая матрица, индексируемая субодиночкой, диагональная.

LaTeX

$$$\text{If } n \text{ is a subsingleton, then } A \text{ is diagonal: } A.IsDiag.$$$

Lean4

/-- Every matrix indexed by a subsingleton is diagonal. -/
theorem isDiag_of_subsingleton [Zero α] [Subsingleton n] (A : Matrix n n α) : A.IsDiag := fun i j h =>
  (h <| Subsingleton.elim i j).elim

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