left_invariant

Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

URI: https://scilib.ai/kg/mathlib#LeftInvariantDerivation.left_invariant

English

The commutator [X,Y] acts on f by X(Yf) - Y(Xf).

Русский

Скобка [X,Y] действует на f как X(Yf) - Y(Xf).

LaTeX

$$$ ⁅X,Y⁆ f = X(Y f) - Y(X f). $$$

Lean4

theorem left_invariant : 𝒅ₕ (smoothLeftMul_one I g) (evalAt (1 : G) X) = evalAt g X :=
  X.left_invariant'' g

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

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

Разделы

Аффилиация

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