instHasTrivialRadicalOfSubsingleton

Mathlib.Algebra.Lie.Semisimple.Defs

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

English

If L is a Subsingleton, then HasTrivialRadical R L holds.

Русский

Если L единична как множество, тогда тривиальный радикал существует.

LaTeX

$$instance [Subsingleton L] : HasTrivialRadical R L$$

Lean4

instance [Subsingleton L] : HasTrivialRadical R L :=
  ⟨by simpa only [radical_eq_top_of_isSolvable] using Subsingleton.elim ⊤ ⊥⟩

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

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

Разделы

Аффилиация

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