charpoly_eq

Mathlib.RingTheory.Invariant.Basic

URI: https://scilib.ai/kg/mathlib#MulSemiringAction.charpoly_eq

English

The characteristic polynomial of a finite group action is monic.

Русский

Характеристический многочлен конечного действия группы монный.

LaTeX

$$$\text{charpoly}(b) \text{ is monic.}$$$

Lean4

theorem charpoly_eq (b : B) : charpoly G b = ∏ g : G, (X - C (g • b)) :=
  rfl

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

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

Разделы

Аффилиация

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