scalar_apply — Mathlib

English

Let a be an element of α. The n-by-n scalar matrix with diagonal entries a (and zeros off the diagonal) coincides with the diagonal matrix whose diagonal is constant a; i.e., the scalar matrix equals the diagonal matrix with all diagonal entries equal to a.

Русский

Пусть a ∈ α. Тогда n×n скалярная матрица со значением a на диагонали и нулями вне диагонали тождественна диагональной матрице с одинаковыми диагональными элементами a.

LaTeX

$$$\mathrm{scalar}_n(a) = \mathrm{diag}(a,\dots,a)$$$

Lean4

@[simp]
theorem scalar_apply (a : α) : scalar n a = diagonal fun _ => a :=
  rfl

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