minpolyDiv_eq_zero

Mathlib.FieldTheory.Minpoly.MinpolyDiv

URI: https://scilib.ai/kg/mathlib#minpolyDiv_eq_zero

← MathLib Explorer

English

The evaluation of minpolyDiv at x matches the derivative-corrected evaluation of minpoly.

Русский

Значение minpolyDiv в x совпадаeт с производной и минимальным полиномом.

LaTeX

$$eval x (minpolyDiv R x) = aeval x (derivative (minpoly R x))$$

Lean4

theorem minpolyDiv_eq_zero (hx : ¬IsIntegral R x) : minpolyDiv R x = 0 :=
  by
  delta minpolyDiv minpoly
  rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]

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

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

Разделы

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

Аффилиация

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