Documentation

Mathlib.RingTheory.Polynomial.Nilpotent

Nilpotency in polynomial rings. #

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

Main results: #

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_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 (P.coeff i)
@[simp]
theorem Polynomial.isNilpotent_reflect_iff {R : Type u_1} [CommRing R] {P : Polynomial R} {N : } (hN : P.natDegree N) :
theorem Polynomial.isUnit_of_coeff_isUnit_isNilpotent {R : Type u_1} [CommRing R] {P : Polynomial R} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ), i 0IsNilpotent (P.coeff i)) :

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 (P.coeff 0) ∀ (i : ), i 0IsNilpotent (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.

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

@[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} :
theorem Polynomial.not_isUnit_of_natDegree_pos_of_isReduced {R : Type u_1} [CommRing R] [IsReduced R] (p : Polynomial R) (hpl : 0 < p.natDegree) :
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)) :
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)) :