lieCharacter_apply_lie

Mathlib.Algebra.Lie.Character

URI: https://scilib.ai/kg/mathlib#LieAlgebra.lieCharacter_apply_lie

← MathLib Explorer

English

For any Lie character χ: L → R and any x,y ∈ L, the value χ([x,y]) is zero.

Русский

Для любого характерa χ: L → R и любых x,y ∈ L выполняется χ([x,y]) = 0.

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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