charpoly_eq_prod_smul

Mathlib.RingTheory.Invariant.Basic

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

English

The characteristic polynomial equals the product over G of (X − g·b).

Русский

Характеристический многочлен равен произведению по G от (X − g·b).

LaTeX

$$$\text{charpoly}(b) = \prod_{g\in G} (X - g\cdot b).$$$

Lean4

theorem charpoly_eq_prod_smul (b : B) : charpoly G b = ∏ g : G, g • (X - C b) := by
  simp only [smul_sub, smul_C, smul_X, charpoly_eq]

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

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

Разделы

Аффилиация

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