English
For K[X], if p is a primitive polynomial over a field K, then its unit behavior is determined by its primitive part and content under localization; specifically, a unit in K[X] arises from a unit in the primitive part and content decomposition.
Русский
Для K[X] примитивный полином имеет единичность, порождаемую примитивной частью и содержимым при локализации; единица в K[X] исходит из единичности примитивной части и содержания.
LaTeX
$$$p^{\\text{IsPrimitive}} \\Rightarrow (\\text{IsUnit}(p) \\iff \\text{IsUnit}(\\text{primitivePart}(p)))$$$
Lean4
theorem isUnit_or_eq_zero_of_isUnit_integerNormalization_primPart {p : K[X]} (h0 : p ≠ 0)
(h : IsUnit (integerNormalization R⁰ p).primPart) : IsUnit p :=
by
rcases isUnit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩
obtain ⟨⟨c, c0⟩, hc⟩ := integerNormalization_map_to_map R⁰ p
rw [Subtype.coe_mk, Algebra.smul_def, algebraMap_apply] at hc
apply isUnit_of_mul_isUnit_right
rw [← hc, (integerNormalization R⁰ p).eq_C_content_mul_primPart, ← hu, ← RingHom.map_mul, isUnit_iff]
refine ⟨algebraMap R K ((integerNormalization R⁰ p).content * ↑u), isUnit_iff_ne_zero.2 fun con => ?_, by simp⟩
replace con := (injective_iff_map_eq_zero (algebraMap R K)).1 (IsFractionRing.injective _ _) _ con
rw [mul_eq_zero, content_eq_zero_iff, IsFractionRing.integerNormalization_eq_zero_iff] at con
rcases con with (con | con)
· apply h0 con
· apply Units.ne_zero _ con
