lie_apply

Mathlib.Algebra.Lie.OfAssociative

URI: https://scilib.ai/kg/mathlib#Module.End.lie_apply

English

The Lie bracket between an endomorphism and a vector is given simply by evaluation: [f, m] = f(m).

Русский

Ли-скобка между эндоморфизмом и вектором задаётся по сути как применение: [f, m] = f(m).

LaTeX

$$$$[f,m] = f(m) \quad (f \in \mathrm{Module.End}, \ m \in M).$$$$

Lean4

@[simp]
theorem lie_apply (f : Module.End R M) (m : M) : ⁅f, m⁆ = f m :=
  rfl

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

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

Разделы

Аффилиация

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