map_lie

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieEquiv.map_lie

English

A Lie equivalence preserves the Lie bracket: e([x,y]) = [e(x), e(y)].

Русский

Эквивелентность Ли сохраняет скобку Ли: e([x,y]) = [e(x), e(y)].

LaTeX

$$$ e([x,y]) = [e(x), e(y)] $$$

Lean4

theorem map_lie (e : L₁ ≃ₗ⁅R⁆ L₂) (x y : L₁) : e ⁅x, y⁆ = ⁅e x, e y⁆ :=
  LieHom.map_lie e.toLieHom x y

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

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

Разделы

Аффилиация

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