English
Let R be an integral domain and p ∈ R[x] be irreducible with deg p > 0. Then p is primitive (the gcd of its coefficients is 1).
Русский
Пусть R — целочисленно-домен, p ∈ R[x] неприводим и имеет положительную степень. Тогда p примитивен (наибольший общий делитель коэффициентов равен 1).
LaTeX
$$$\text{If } R \text{ is an integral domain and } p \in R[X] \text{ irreducible with } \deg p > 0,\ \operatorname{cont}(p)=1.$$$
Lean4
/-- An irreducible nonconstant polynomial over a domain is primitive. -/
theorem _root_.Irreducible.isPrimitive [NoZeroDivisors R] {p : Polynomial R} (hp : Irreducible p)
(hp' : p.natDegree ≠ 0) : p.IsPrimitive := by
rintro r ⟨q, hq⟩
suffices ¬IsUnit q by simpa using ((hp.2 hq).resolve_right this).map Polynomial.constantCoeff
intro H
have hr : r ≠ 0 := by rintro rfl; simp_all
obtain ⟨s, hs, rfl⟩ := Polynomial.isUnit_iff.mp H
simp [hq, Polynomial.natDegree_C_mul hr] at hp'
