instSMul

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieModuleHom.instSMul

English

Natural-number scalar multiplication is defined on LieModuleHom by n • f, with (n • f) m = n • f m.

Русский

Натуральное число действует на LieModuleHom так: n • f, и (n • f) m = n • f m.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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