add_apply

Mathlib.Algebra.Lie.Basic

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

English

For f, g : M →ₗ⁅R,L⁆ N and m ∈ M, the evaluation distributes over addition: (f+g) m = f m + g m.

Русский

Для f, g : M →ₗ⁅R,L⁆ N и m ∈ M вектор-применение к сумме распадается как сумма применений: (f+g) m = f m + g m.

LaTeX

$$$ (f+g)(m) = f(m) + g(m) $$$

Lean4

theorem add_apply (f g : M →ₗ⁅R,L⁆ N) (m : M) : (f + g) m = f m + g m :=
  rfl

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

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

Разделы

Аффилиация

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