lieCharpoly_monic

Mathlib.Algebra.Lie.CartanExists

URI: https://scilib.ai/kg/mathlib#LieAlgebra.engel_isBot_of_isMin.lieCharpoly_monic

English

The lieCharpoly is monic in x for the given Lie algebra/module data.

Русский

lieCharpoly по данным Ли-алгебры и модуля является монотонной по переменной x.

LaTeX

$$(lieCharpoly R M x y).Monic$$

Lean4

theorem lieCharpoly_monic : (lieCharpoly R M x y).Monic :=
  (polyCharpoly_monic _ _).map _

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

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

Разделы

Аффилиация

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