smul_charpoly

Mathlib.RingTheory.Invariant.Basic

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

English

The action by g on the charpoly is the same as the charpoly itself: smul by g fixes the polynomial.

Русский

Действие элемента g на характеристический многочлен не изменяет его.

LaTeX

$$$g \cdot \text{charpoly}(b) = \text{charpoly}(b)$ for all g in G.$$

Lean4

theorem smul_charpoly (b : B) (g : G) : g • (charpoly G b) = charpoly G b := by
  rw [charpoly_eq_prod_smul, Finset.smul_prod_perm]

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

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

Разделы

Аффилиация

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