map_lie

Mathlib.Algebra.Lie.Basic

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

English

LieHom preserves brackets: f([x,y]) = [f(x), f(y)].

Русский

LieHom сохраняет скобку Ли: f([x,y]) = [f(x), f(y)].

LaTeX

$$$f \,[x,y]\;=\; [f x, f y]$$$

Lean4

@[simp]
theorem map_lie (f : L₁ →ₗ⁅R⁆ L₂) (x y : L₁) : f ⁅x, y⁆ = ⁅f x, f y⁆ :=
  LieHom.map_lie' f

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

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

Разделы

Аффилиация

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