map_smulₛₗ

Mathlib.Algebra.Module.LinearMap.Defs

URI: https://scilib.ai/kg/mathlib#LinearMap.map_smulₛₗ

English

For a σ-linear map f from M to M₃, f(c • x) = σ(c) • f(x) for all c in R and x in M.

Русский

Для σ-линейного отображения f: M → M₃ выполняется f(c • x) = σ(c) • f(x) для всех c ∈ R и x ∈ M.

LaTeX

$$$ f \bigl(c \cdot x\bigr) = \sigma(c) \cdot f(x) $$$

Lean4

@[simp]
protected theorem map_smulₛₗ (c : R) (x : M) : f (c • x) = σ c • f x :=
  map_smulₛₗ f c x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru