dvd_iff

Mathlib.FieldTheory.Minpoly.Field

URI: https://scilib.ai/kg/mathlib#minpoly.dvd_iff

English

minpoly A x ∣ p iff aeval x p = 0.

Русский

minpoly A x делит p тогда и только тогда, когда aeval x p = 0.

LaTeX

$$$\\minpoly A x \\mid p \\; \\iff \\; \\operatorname{aeval} x p = 0$$$

Lean4

theorem dvd_iff {p : A[X]} : minpoly A x ∣ p ↔ Polynomial.aeval x p = 0 :=
  ⟨fun ⟨q, hq⟩ ↦ by rw [hq, map_mul, aeval, zero_mul], minpoly.dvd A x⟩

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

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

Разделы

Аффилиация

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