map_smul — Mathlib

English

For any F fitting the LinearMapClass, the map_smul law holds: f (r • x) = r • f x.

Русский

Для любого F, удовлетворяющего LinearMapClass, выполняется свойство map_smul: f (r • x) = r • f x.

LaTeX

$$$f(r\cdot x) = r\cdot f(x)$$$

Lean4

protected theorem map_smul {R M M₂ : outParam Type*} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M]
    [Module R M₂] {F : Type*} [FunLike F M M₂] [LinearMapClass F R M M₂] (f : F) (r : R) (x : M) :
    f (r • x) = r • f x := by rw [map_smul]

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