lieCharacter_apply_lie' — Mathlib

English

For a Lie character χ, the Lie bracket of χ(x) and χ(y) in the base ring is zero for all x,y.

Русский

Для характеристи Ли χ скобка [χ(x), χ(y)] в базовом кольце равна нулю для всех x,y.

LaTeX

$$$$ [\chi(x), \chi(y)] = 0 \quad \text{for all } x,y \in L. $$$$

Lean4

@[simp]
theorem lieCharacter_apply_lie' (χ : LieCharacter R L) (x y : L) : ⁅χ x, χ y⁆ = 0 := by
  rw [LieRing.of_associative_ring_bracket, mul_comm, sub_self]

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