radical_eq_top_of_isSolvable

Mathlib.Algebra.Lie.Solvable

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

← MathLib Explorer

English

If L is solvable, then its radical equals the top subalgebra.

Русский

Если L разрешима, то радикал L равен верхнему подполя (Top).

LaTeX

$$$\text{IsSolvable } L \Rightarrow \operatorname{radical} R L = \top$$$

Lean4

@[simp]
theorem radical_eq_top_of_isSolvable [IsSolvable L] : radical R L = ⊤ :=
  by
  rw [eq_top_iff]
  have h : IsSolvable (⊤ : LieSubalgebra R L) := inferInstance
  exact le_sSup h

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

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

Разделы

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

Аффилиация

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