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)

theorem Polynomial.not_isUnit_of_natDegree_pos_of_isReduced {R : Type u_1} [CommRing R] [IsReduced R] (p : Polynomial R) (hpl : 0 < Polynomial.natDegree p) : ¬IsUnit p

theorem Polynomial.not_isUnit_of_degree_pos_of_isReduced {R : Type u_1} [CommRing R] [IsReduced R] (p : Polynomial R) (hpl : 0 < Polynomial.degree p) : ¬IsUnit p

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 : S} {b : S} (h : IsNilpotent (a - b)) : IsNilpotent ((Polynomial.aeval a) P - (Polynomial.aeval b) P)

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 : S} {b : S} (hb : IsUnit ((Polynomial.aeval b) P)) (hab : IsNilpotent (a - b)) : IsUnit ((Polynomial.aeval a) P)