Nilpotency in polynomial rings.

This file is a place for results related to nilpotency in (single-variable) polynomial rings.

Main results:

• Polynomial.isNilpotent_iff
• Polynomial.isUnit_iff_coeff_isUnit_isNilpotent

theorem Polynomial.isNilpotent_C_mul_pow_X_of_isNilpotent {R : Type u_1} {r : R} [Semiring R] (n : ℕ) (hnil : IsNilpotent r) : IsNilpotent (↑Polynomial.C r * Polynomial.X ^ n)

theorem Polynomial.isNilpotent_pow_X_mul_C_of_isNilpotent {R : Type u_1} {r : R} [Semiring R] (n : ℕ) (hnil : IsNilpotent r) : IsNilpotent (Polynomial.X ^ n * ↑Polynomial.C r)

@[simp]

theorem Polynomial.isNilpotent_monomial_iff {R : Type u_1} {r : R} [Semiring R] {n : ℕ} : IsNilpotent (↑(Polynomial.monomial n) r) ↔ IsNilpotent r

@[simp]

theorem Polynomial.isNilpotent_C_iff {R : Type u_1} {r : R} [Semiring R] : IsNilpotent (↑Polynomial.C r) ↔ IsNilpotent r

@[simp]

theorem Polynomial.isNilpotent_X_mul_iff {R : Type u_1} [Semiring R] {P : Polynomial R} : IsNilpotent (Polynomial.X * P) ↔ IsNilpotent P

@[simp]

theorem Polynomial.isNilpotent_mul_X_iff {R : Type u_1} [Semiring R] {P : Polynomial R} : IsNilpotent (P * Polynomial.X) ↔ IsNilpotent P

theorem Polynomial.isNilpotent_iff {R : Type u_1} [CommRing R] {P : Polynomial R} : IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (Polynomial.coeff P i)

@[simp]

theorem Polynomial.isNilpotent_reflect_iff {R : Type u_1} [CommRing R] {P : Polynomial R} {N : ℕ} (hN : Polynomial.natDegree P ≤ N) : IsNilpotent (Polynomial.reflect N P) ↔ IsNilpotent P

@[simp]

theorem Polynomial.isNilpotent_reverse_iff {R : Type u_1} [CommRing R] {P : Polynomial R} : IsNilpotent (Polynomial.reverse P) ↔ IsNilpotent P

theorem Polynomial.isUnit_of_coeff_isUnit_isNilpotent {R : Type u_1} [CommRing R] {P : Polynomial R} (hunit : IsUnit (Polynomial.coeff P 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (Polynomial.coeff P i)) : IsUnit P

Let P be a polynomial over R. If its constant term is a unit and its other coefficients are nilpotent, then P is a unit.

See also Polynomial.isUnit_iff_coeff_isUnit_isNilpotent.

theorem Polynomial.coeff_isUnit_isNilpotent_of_isUnit {R : Type u_1} [CommRing R] {P : Polynomial R} (hunit : IsUnit P) : IsUnit (Polynomial.coeff P 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (Polynomial.coeff P i)

Let P be a polynomial over R. If P is a unit, then all its coefficients are nilpotent, except its constant term which is a unit.

See also Polynomial.isUnit_iff_coeff_isUnit_isNilpotent.

theorem Polynomial.isUnit_iff_coeff_isUnit_isNilpotent {R : Type u_1} [CommRing R] {P : Polynomial R} : IsUnit P ↔ IsUnit (Polynomial.coeff P 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (Polynomial.coeff P i)

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'.

@[simp]

theorem Polynomial.isUnit_C_add_X_mul_iff {R : Type u_1} {r : R} [CommRing R] {P : Polynomial R} : IsUnit (↑Polynomial.C r + Polynomial.X * P) ↔ IsUnit r ∧ IsNilpotent P

theorem Polynomial.isUnit_iff' {R : Type u_1} [CommRing R] {P : Polynomial R} : IsUnit P ↔ IsUnit (Polynomial.eval 0 P) ∧ IsNilpotent (P /ₘ Polynomial.X)