ad_ker_eq_bot_of_hasTrivialRadical

Mathlib.Algebra.Lie.Semisimple.Basic

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

English

The kernel of the adjoint representation is zero for HasTrivialRadical.

Русский

Ядро представления адъюнкта равно нулю при тривиальном радикале.

LaTeX

$$$(ad\; R\; L).ker = \bot$$

Lean4

theorem ad_ker_eq_bot_of_hasTrivialRadical [HasTrivialRadical R L] : (ad R L).ker = ⊥ := by simp

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

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

Разделы

Аффилиация

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