isUnit_iff_coeff_isUnit_isNilpotent

English

A polynomial P ∈ R[X] is a unit if and only if its constant term is a unit and every other coefficient is nilpotent.

Русский

Полином P ∈ R[X] является единицей тогда и только тогда, когда его коэффициент нулевой степени является единицей, а все остальные коэффициенты нильпотентны.

LaTeX

$$$\operatorname{IsUnit}(P) \iff \operatorname{IsUnit}(P.\text{coeff }0) \land \forall i \,(i \neq 0 \rightarrow \operatorname{IsNilpotent}(P.\text{coeff }i))$$$

Lean4

/-- Let `P` be a polynomial over `R`. `P` is a unit if and only if all its coefficients are
nilpotent, except its constant term which is a unit.

See also `Polynomial.isUnit_iff'`. -/
theorem isUnit_iff_coeff_isUnit_isNilpotent : IsUnit P ↔ IsUnit (P.coeff 0) ∧ (∀ i, i ≠ 0 → IsNilpotent (P.coeff i)) :=
  ⟨coeff_isUnit_isNilpotent_of_isUnit, fun H => isUnit_of_coeff_isUnit_isNilpotent H.1 H.2⟩

Похожие утверждения