hasNSMul — Mathlib

English

The natural-number scalar action is defined on LieModuleHom by n • f, with (n • f)(m) = n • f(m).

Русский

Действие естественных чисел на гомоморфизмах Ли задаётся так: n • f, и (n • f)(m) = n • f(m).

LaTeX

$$$\forall n \in \mathbb{N}, \forall m \in M:\ (n \cdot f)(m) = n \cdot f(m)$$$

Lean4

instance hasNSMul : SMul ℕ (M →ₗ⁅R,L⁆ N) where smul n f := { n • (f : M →ₗ[R] N) with map_lie' := by simp }

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