eq_iff_aeval_eq_zero — Mathlib

English

If p ∈ A[X] is irreducible, p(x) = 0, and p is monic, then p equals the minimal polynomial of x over A.

Русский

Если p ирредуцируемый над A[X], p(x) = 0 и p монический, то p совпадает с минимальным полиномом x над A.

LaTeX

$$Irreducible p ∧ p.Monic ∧ Polynomial.aeval x p = 0 ⇒ p = minpoly A x$$

Lean4

theorem eq_iff_aeval_eq_zero [Nontrivial B] {p : A[X]} (irr : Irreducible p) (monic : p.Monic) :
    p = minpoly A x ↔ Polynomial.aeval x p = 0 :=
  ⟨(· ▸ aeval A x), (eq_of_irreducible_of_monic irr · monic)⟩

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