prime — Mathlib

English

If x ∈ B is integral over A, then minpoly_A x is a prime polynomial.

Русский

Если x ∈ B интеграл над A, то minpoly_A x является простым полиномом.

LaTeX

$$Irreducible (minpoly A x) ∧ Monic (minpoly A x) ⇒ Prime (minpoly A x)$$

Lean4

/-- A minimal polynomial is prime. -/
theorem prime (hx : IsIntegral A x) : Prime (minpoly A x) :=
  by
  refine ⟨minpoly.ne_zero hx, not_isUnit A x, ?_⟩
  rintro p q ⟨d, h⟩
  have : Polynomial.aeval x (p * q) = 0 := by simp [h, aeval A x]
  replace : Polynomial.aeval x p = 0 ∨ Polynomial.aeval x q = 0 := by simpa
  exact Or.imp (dvd A x) (dvd A x) this

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