add_lie

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#add_lie

English

The Lie bracket is additive in the first argument: [x+y, m] = [x,m] + [y,m].

Русский

Скобка Ли линейна по первому аргументу: ⁅x+y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆.

LaTeX

$$$ [x+y, m] = [x,m] + [y,m] $$$

Lean4

@[simp]
theorem add_lie : ⁅x + y, m⁆ = ⁅x, m⁆ + ⁅y, m⁆ :=
  LieRingModule.add_lie x y m

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

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

Разделы

Аффилиация

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