eq_of_irreducible_of_monic — Mathlib

English

Let B be nontrivial. If p ∈ A[X] is irreducible, p is monic, and p(x) = 0 for some x ∈ B, then p = minpoly_A(x).

Русский

Пусть B неоднозначно не тривиально; если p ∈ A[X] ирредуцируем и монический и p(x) = 0 для некоторого x ∈ B, то p = minpoly_A(x).

LaTeX

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

Lean4

theorem eq_of_irreducible_of_monic [Nontrivial B] {p : A[X]} (hp1 : Irreducible p) (hp2 : Polynomial.aeval x p = 0)
    (hp3 : p.Monic) : p = minpoly A x :=
  let ⟨_, hq⟩ := dvd A x hp2
  eq_of_monic_of_associated hp3 (monic ⟨p, ⟨hp3, hp2⟩⟩) <|
    mul_one (minpoly A x) ▸
      hq.symm ▸
        Associated.mul_left _ (associated_one_iff_isUnit.2 <| (hp1.isUnit_or_isUnit hq).resolve_left <| not_isUnit A x)

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