nsmul_apply

Mathlib.Algebra.Lie.Basic

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

English

For n ∈ ℕ, f : M →ₗ⁅R,L⁆ N, and m ∈ M, (n • f) m = n • f m.

Русский

Для n ∈ ℕ, f : M →ₗ⁅R,L⁆ N и m ∈ M имеем (n • f) m = n • f m.

LaTeX

$$$ (n \cdot f)(m) = n \cdot f(m)$$$

Lean4

theorem nsmul_apply (n : ℕ) (f : M →ₗ⁅R,L⁆ N) (m : M) : (n • f) m = n • f m :=
  rfl

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

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

Разделы

Аффилиация

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