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

• Polynomial.isNilpotent_iff
• Polynomial.isUnit_iff_coeff_isUnit_isNilpotent
theorem Polynomial.isNilpotent_C_mul_pow_X_of_isNilpotent {R : Type u_1} {r : R} [] (n : ) (hnil : ) :
IsNilpotent (Polynomial.C r * Polynomial.X ^ n)
theorem Polynomial.isNilpotent_pow_X_mul_C_of_isNilpotent {R : Type u_1} {r : R} [] (n : ) (hnil : ) :
IsNilpotent (Polynomial.X ^ n * Polynomial.C r)
@[simp]
theorem Polynomial.isNilpotent_monomial_iff {R : Type u_1} {r : R} [] {n : } :
IsNilpotent (↑() r)
@[simp]
theorem Polynomial.isNilpotent_C_iff {R : Type u_1} {r : R} [] :
IsNilpotent (Polynomial.C r)
@[simp]
theorem Polynomial.isNilpotent_X_mul_iff {R : Type u_1} [] {P : } :
IsNilpotent (Polynomial.X * P)
@[simp]
theorem Polynomial.isNilpotent_mul_X_iff {R : Type u_1} [] {P : } :
IsNilpotent (P * Polynomial.X)
theorem Polynomial.isNilpotent_iff {R : Type u_1} [] {P : } :
∀ (i : ),
@[simp]
theorem Polynomial.isNilpotent_reflect_iff {R : Type u_1} [] {P : } {N : } (hN : ) :
@[simp]
theorem Polynomial.isNilpotent_reverse_iff {R : Type u_1} [] {P : } :
theorem Polynomial.isUnit_of_coeff_isUnit_isNilpotent {R : Type u_1} [] {P : } (hunit : IsUnit ()) (hnil : ∀ (i : ), i 0) :

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} [] {P : } (hunit : ) :
IsUnit () ∀ (i : ), i 0

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} [] {P : } :
IsUnit () ∀ (i : ), i 0

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} [] {P : } :
IsUnit (Polynomial.C r + Polynomial.X * P)
theorem Polynomial.isUnit_iff' {R : Type u_1} [] {P : } :
IsUnit () IsNilpotent (P /ₘ Polynomial.X)