eval_charpoly

Mathlib.RingTheory.Invariant.Basic

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

← MathLib Explorer

English

Evaluating the charpoly at b yields zero.

Русский

Пусть при подстановке b характеристический многочлен даёт ноль.

LaTeX

$$$\text{charpoly}(G,b)\big|_{X=b}=0$$$

Lean4

theorem eval_charpoly (b : B) : (charpoly G b).eval b = 0 :=
  by
  rw [charpoly_eq, eval_prod]
  apply Finset.prod_eq_zero (Finset.mem_univ (1 : G))
  rw [one_smul, eval_sub, eval_C, eval_X, sub_self]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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