# 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`

source
theorem Polynomial.isNilpotent_C_mul_pow_X_of_isNilpotent {R : Type u_1} {r : R} [Semiring R] (n : ℕ) (hnil : IsNilpotent r) :
IsNilpotent (C r * X ^ n)
source
theorem Polynomial.isNilpotent_pow_X_mul_C_of_isNilpotent {R : Type u_1} {r : R} [Semiring R] (n : ℕ) (hnil : IsNilpotent r) :
IsNilpotent (X ^ n * C r)
source
@[simp]
theorem Polynomial.isNilpotent_monomial_iff {R : Type u_1} {r : R} [Semiring R] {n : ℕ} :
IsNilpotent ((monomial n) r) ↔ IsNilpotent r
source
@[simp]
theorem Polynomial.isNilpotent_C_iff {R : Type u_1} {r : R} [Semiring R] :
IsNilpotent (C r) ↔ IsNilpotent r
source
@[simp]
theorem Polynomial.isNilpotent_X_mul_iff {R : Type u_1} [Semiring R] {P : Polynomial R} :
IsNilpotent (X * P) ↔ IsNilpotent P
source
@[simp]
theorem Polynomial.isNilpotent_mul_X_iff {R : Type u_1} [Semiring R] {P : Polynomial R} :
IsNilpotent (P * X) ↔ IsNilpotent P
source
theorem Polynomial.isNilpotent_iff {R : Type u_1} [CommRing R] {P : Polynomial R} :
IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
source
@[simp]
theorem Polynomial.isNilpotent_reflect_iff {R : Type u_1} [CommRing R] {P : Polynomial R} {N : ℕ} (hN : P.natDegree ≤ N) :
IsNilpotent (reflect N P) ↔ IsNilpotent P
source
@[simp]
theorem Polynomial.isNilpotent_reverse_iff {R : Type u_1} [CommRing R] {P : Polynomial R} :
IsNilpotent P.reverse ↔ IsNilpotent P
source
theorem Polynomial.isUnit_of_coeff_isUnit_isNilpotent {R : Type u_1} [CommRing R] {P : Polynomial R} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff 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`.

source
theorem Polynomial.coeff_isUnit_isNilpotent_of_isUnit {R : Type u_1} [CommRing R] {P : Polynomial R} (hunit : IsUnit P) :
IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff 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`.

source
theorem Polynomial.isUnit_iff_coeff_isUnit_isNilpotent {R : Type u_1} [CommRing R] {P : Polynomial R} :
IsUnit P ↔ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff 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'`.

source
@[simp]
theorem Polynomial.isUnit_C_add_X_mul_iff {R : Type u_1} {r : R} [CommRing R] {P : Polynomial R} :
IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P
source
theorem Polynomial.isUnit_iff' {R : Type u_1} [CommRing R] {P : Polynomial R} :
IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
source
theorem Polynomial.not_isUnit_of_natDegree_pos_of_isReduced {R : Type u_1} [CommRing R] [IsReduced R] (p : Polynomial R) (hpl : 0 < p.natDegree) :
¬IsUnit p
source
theorem Polynomial.not_isUnit_of_degree_pos_of_isReduced {R : Type u_1} [CommRing R] [IsReduced R] (p : Polynomial R) (hpl : 0 < p.degree) :
¬IsUnit p
source
theorem Polynomial.isNilpotent_aeval_sub_of_isNilpotent_sub {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (P : Polynomial R) {a b : S} (h : IsNilpotent (a - b)) :
IsNilpotent ((aeval a) P - (aeval b) P)
source
theorem Polynomial.isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {a b : S} (hb : IsUnit ((aeval b) P)) (hab : IsNilpotent (a - b)) :
IsUnit ((aeval a) P)