lie_mem_left

Mathlib.Algebra.Lie.Ideal

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

English

If x ∈ I and y ∈ L, then [x,y] ∈ I.

Русский

Если x ∈ I и y ∈ L, то [x,y] ∈ I.

LaTeX

$$$\forall x \in I, y \in L:\; [x,y] \in I.$$$

Lean4

theorem lie_mem_left (I : LieIdeal R L) (x y : L) (h : x ∈ I) : ⁅x, y⁆ ∈ I := by rw [← lie_skew, ← neg_lie];
  apply lie_mem_right; assumption

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

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

Разделы

Аффилиация

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