English
Let R be a ring with no zero divisors. A polynomial p ∈ R[X] is a unit in R[X] if and only if p is a constant unit of R; equivalently p = C r for some unit r ∈ R.
Русский
Пусть R — кольцо без нулевых делителей. Полином p ∈ R[X] является единицей в R[X] тогда и только тогда, когда p является константой, равной единице элемента R; эквивалентно p = C(r) для некоторой единицы r ∈ R.
LaTeX
$$$\IsUnit(p) \iff \exists r \in R, \IsUnit(r) \land p = C r$$$
Lean4
/-- Characterization of a unit of a polynomial ring over an integral domain `R`.
See `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent` when `R` is a commutative ring. -/
theorem isUnit_iff : IsUnit p ↔ ∃ r : R, IsUnit r ∧ C r = p :=
⟨fun hp =>
⟨p.coeff 0,
let h := eq_C_of_natDegree_eq_zero (natDegree_eq_zero_of_isUnit hp)
⟨isUnit_C.1 (h ▸ hp), h.symm⟩⟩,
fun ⟨_, hr, hrp⟩ => hrp ▸ isUnit_C.2 hr⟩
