of_smul — Mathlib

English

Inclusion map commutes with scalar multiplication: of_i (c • x) = c • of_i x.

Русский

Включение i-го компонента коммутирует с умножением на скаляр: of_i(c•x) = c•of_i x.

LaTeX

$$$\\mathrm{of}\\; M_i\\; (c \\cdot x) = c \\cdot \\mathrm{of}\\; M_i\\; x$$$

Lean4

/-- Scalar multiplication commutes with the inclusion of each component into the direct sum. -/
theorem of_smul (i : ι) (c : R) (x) : of M i (c • x) = c • of M i x :=
  (lof R ι M i).map_smul c x

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