prime_of_isIntegrallyClosed — Mathlib

English

Another formulation of the uniqueness of minpoly under IsIntegrallyClosed.

Русский

Другая формулировка уникальности минполинома при IsIntegrallyClosed.

LaTeX

$$$\text{IsIntegrallyClosed.minpoly.unique}$ (alternative form)$$

Lean4

theorem prime_of_isIntegrallyClosed {x : S} (hx : IsIntegral R x) : Prime (minpoly R x) :=
  by
  refine
    ⟨(minpoly.monic hx).ne_zero,
      ⟨fun h_contra => (ne_of_lt (minpoly.degree_pos hx)) (degree_eq_zero_of_isUnit h_contra).symm, fun a b h =>
        or_iff_not_imp_left.mpr fun h' => ?_⟩⟩
  rw [← minpoly.isIntegrallyClosed_dvd_iff hx] at h' h ⊢
  rw [aeval_mul] at h
  exact eq_zero_of_ne_zero_of_mul_left_eq_zero h' h

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