prime_of_degree_eq_one — Mathlib

English

Let R be a domain. If p ∈ R[X] has degree 1 and is monic, then p is prime in R[X].

Русский

Пусть R — область. Любой полином p ∈ R[X] с deg(p) = 1 и monic является простым в R[X].

LaTeX

$$$\deg(p) = 1 \wedge p \text{ is Monic} \Rightarrow p \text{ is Prime in } R[X].$$$

Lean4

theorem prime_of_degree_eq_one (hp1 : degree p = 1) (hm : Monic p) : Prime p :=
  have : p = X - C (-p.coeff 0) := by simpa [hm.leadingCoeff] using eq_X_add_C_of_degree_eq_one hp1
  this.symm ▸ prime_X_sub_C _

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