English
The primitive part of a constant polynomial C r is a unit (in particular, equals a unit when r ≠ 0).
Русский
Примитивная часть константного многочлена C r является единицей (при r ≠ 0 равна единственной единице по нормализации).
LaTeX
$$$IsUnit\bigl((C r).primPart\bigr)$$$
Lean4
theorem isUnit_primPart_C (r : R) : IsUnit (C r).primPart :=
by
by_cases h0 : r = 0
· simp [h0]
unfold IsUnit
refine
⟨⟨C ↑(normUnit r)⁻¹, C ↑(normUnit r), by rw [← RingHom.map_mul, Units.inv_mul, C_1], by
rw [← RingHom.map_mul, Units.mul_inv, C_1]⟩,
?_⟩
rw [← normalize_eq_zero, ← C_eq_zero] at h0
apply mul_left_cancel₀ h0
conv_rhs => rw [← content_C, ← (C r).eq_C_content_mul_primPart]
simp only [normalize_apply, RingHom.map_mul]
rw [mul_assoc, ← RingHom.map_mul, Units.mul_inv, C_1, mul_one]
