engel_zero

Mathlib.Algebra.Lie.EngelSubalgebra

URI: https://scilib.ai/kg/mathlib#LieSubalgebra.engel_zero

← MathLib Explorer

English

The Engel subalgebra of the zero element is the whole Lie algebra, i.e., engel(R, 0) = ⊤.

Русский

Энгель подалгебра нуля равна всей алгебре: engel(R, 0) = ⊤.

LaTeX

$$$\operatorname{engel}(R,0) = \top$$$

Lean4

@[simp]
theorem engel_zero : engel R (0 : L) = ⊤ := by
  rw [eq_top_iff]
  rintro x -
  rw [mem_engel_iff, LieHom.map_zero]
  use 1
  simp only [pow_one, LinearMap.zero_apply]

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

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

Разделы

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

Аффилиация

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