lie_apply

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieHom.lie_apply

English

There is a Lie bracket on the space of linear maps M →ᴿ N given by ([x,f])(m) = [x, f(m)] − f([x,m]).

Русский

На пространстве линейных отображений действует скобка Ли: ([x,f])(m) = [x, f(m)] − f([x,m]).

LaTeX

$$$[x,f] = (m \mapsto [x, f(m)] - f([x,m]))$$$

Lean4

@[simp]
theorem lie_apply (f : M →ₗ[R] N) (x : L) (m : M) : ⁅x, f⁆ m = ⁅x, f m⁆ - f ⁅x, m⁆ :=
  rfl

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

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

Разделы

Аффилиация

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