diagonal_smul — Mathlib

English

A scalar acts diagonally as a scalar multiple of the diagonal matrix.

Русский

Скаляр действует на диагональную матрицу как скалярный множитель диагонали.

LaTeX

$$$\\mathrm{diag}(r \\cdot d) = r \\cdot \\mathrm{diag}(d)$$$

Lean4

@[simp]
theorem diagonal_smul [Zero α] [SMulZeroClass R α] (r : R) (d : n → α) : diagonal (r • d) = r • diagonal d :=
  by
  ext i j
  by_cases h : i = j <;> simp [h]

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