sub_lie

Mathlib.Algebra.Lie.Basic

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

English

The bracket is linear 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 sub_lie : ⁅x - y, m⁆ = ⁅x, m⁆ - ⁅y, m⁆ := by simp [sub_eq_add_neg]

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

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

Разделы

Аффилиация

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