prime_of_degree_eq_one — Mathlib

English

If deg p = 1, then p is prime in the polynomial ring over a field.

Русский

Если deg p = 1, то p — простый полином в кольце полиномов над полем.

LaTeX

$$deg p = 1 → Prime p$$

Lean4

theorem prime_of_degree_eq_one (hp1 : degree p = 1) : Prime p := by
  classical
  have : Prime (normalize p) :=
    Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
      (monic_normalize fun hp0 => absurd hp1 (hp0.symm ▸ by simp [degree_zero]))
  exact (normalize_associated _).prime this

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