English
Let R be a commutative ring, and r ∈ R and P ∈ R[X]. Then C r + X P is a unit in R[X] if and only if r is a unit in R and P is nilpotent.
Русский
Пусть R — коммутативное кольцо, r ∈ R и P ∈ R[X]. Тогда Cr + X P является единицей в R[X] тогда и только тогда, когда r является единицей в R и P нильпотентен.
LaTeX
$$$\operatorname{IsUnit}(\,C r + X P\,) \iff \operatorname{IsUnit}(r) \land \operatorname{IsNilpotent}(P)$$$
Lean4
@[simp]
theorem isUnit_C_add_X_mul_iff : IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P :=
by
have : ∀ i, coeff (C r + X * P) (i + 1) = coeff P i := by simp
simp_rw [isUnit_iff_coeff_isUnit_isNilpotent, Nat.forall_ne_zero_iff, this]
simp only [coeff_add, coeff_C_zero, mul_coeff_zero, coeff_X_zero, zero_mul, add_zero, ← Polynomial.isNilpotent_iff]
