zsmul_apply

Mathlib.Algebra.Lie.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem zsmul_apply (z : ℤ) (f : M →ₗ⁅R,L⁆ N) (m : M) : (z • f) m = z • f m :=
  rfl

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

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

Разделы

Аффилиация

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