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

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.

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} :