isDiag_smul_one — Mathlib

English

A scalar multiple of the identity matrix is diagonal; in particular, k times the identity is diagonal.

Русский

Любое скалярное кратное единичной матрице диагонально.

LaTeX

$$$\\forall {\\alpha} (n) [MulZeroOneClass \\alpha] [DecidableEq n] (k : \u03b1) : (k \\u22a5 (1 : Matrix n n \\alpha)).IsDiag$$$

Lean4

@[simp]
theorem isDiag_smul_one (n) [MulZeroOneClass α] [DecidableEq n] (k : α) : (k • (1 : Matrix n n α)).IsDiag :=
  isDiag_one.smul k

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