toMatrix_lsmul — Mathlib

English

The matrix of smul by x (as a linear map) is diagonal with x on the diagonal.

Русский

Матрица умножения на x (через smul) — диагональная с x на диагонали.

LaTeX

$$$\operatorname{toMatrix}_{b b}(\mathrm{Algebra.lsmul}\; R\; S\; x) = \operatorname{diagonal}(\lambda\;. x).$$$

Lean4

@[simp]
theorem toMatrix_lsmul (x : R) : LinearMap.toMatrix b b (Algebra.lsmul R R S x) = Matrix.diagonal fun _ ↦ x :=
  toMatrix_distrib_mul_action_toLinearMap b x

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