map_zsmul_unit — Mathlib

English

Any F with compatible SMul and LinearMapClass satisfies the tower property for smul operations.

Русский

Любой F с совместимой областью скаляров и классом линейных отображений удовлетворяет свойствам башни для скаляров.

LaTeX

$$$ f_\ell (c \cdot x) = c \cdot f_\ell x $$$

Lean4

@[simp]
theorem _root_.map_zsmul_unit {F M N : Type*} [AddGroup M] [AddGroup N] [FunLike F M N] [AddMonoidHomClass F M N]
    (f : F) (c : ℤˣ) (m : M) : f (c • m) = c • f m := by simp [Units.smul_def]

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