# Documentation

Mathlib.RingTheory.Nilpotent

# Nilpotent elements #

## Main definitions #

• IsNilpotent
• isNilpotent_neg_iff
• Commute.isNilpotent_add
• Commute.isNilpotent_mul_left
• Commute.isNilpotent_mul_right
• Commute.isNilpotent_sub
def IsNilpotent {R : Type u_1} [Zero R] [Pow R ] (x : R) :

An element is said to be nilpotent if some natural-number-power of it equals zero.

Note that we require only the bare minimum assumptions for the definition to make sense. Even MonoidWithZero is too strong since nilpotency is important in the study of rings that are only power-associative.

Instances For
theorem IsNilpotent.mk {R : Type u_1} [Zero R] [Pow R ] (x : R) (n : ) (e : x ^ n = 0) :
@[simp]
theorem IsNilpotent.zero {R : Type u_1} [] :
theorem IsNilpotent.neg {R : Type u_1} {x : R} [Ring R] (h : ) :
theorem IsNilpotent.pow {n : } {S : Type u_3} [] {x : S} (hx : ) :
theorem IsNilpotent.pow_of_pos {n : } {S : Type u_3} [] {x : S} (hx : ) (hn : n 0) :
@[simp]
theorem isNilpotent_neg_iff {R : Type u_1} {x : R} [Ring R] :
theorem IsNilpotent.map {R : Type u_1} {S : Type u_2} [] [] {r : R} {F : Type u_3} [] (hr : ) (f : F) :
IsNilpotent (f r)
theorem IsNilpotent.sub_one_isUnit {R : Type u_1} [Ring R] {r : R} (hnil : ) :
IsUnit (r - 1)
theorem Commute.IsNilpotent.add_isUnit {R : Type u_1} [Ring R] {r : R} {u : Rˣ} (hnil : ) (hru : Commute r u⁻¹) :
IsUnit (u + r)
theorem isReduced_iff (R : Type u_3) [Zero R] [Pow R ] :
∀ (x : R), x = 0
class IsReduced (R : Type u_3) [Zero R] [Pow R ] :
• eq_zero : ∀ (x : R), x = 0

A reduced structure has no nonzero nilpotent elements.

A structure that has zero and pow is reduced if it has no nonzero nilpotent elements.

Instances
instance isReduced_of_noZeroDivisors {R : Type u_1} [] [] :
instance isReduced_of_subsingleton {R : Type u_1} [Zero R] [Pow R ] [] :
theorem IsNilpotent.eq_zero {R : Type u_1} {x : R} [Zero R] [Pow R ] [] (h : ) :
x = 0
@[simp]
theorem isNilpotent_iff_eq_zero {R : Type u_1} {x : R} [] [] :
x = 0
theorem isReduced_of_injective {R : Type u_1} {S : Type u_2} [] [] {F : Type u_3} [] (f : F) (hf : ) [] :
theorem RingHom.ker_isRadical_iff_reduced_of_surjective {R : Type u_1} {S : Type u_3} {F : Type u_4} [] [] [RingHomClass F R S] {f : F} (hf : ) :
def IsRadical {R : Type u_1} [Dvd R] [Pow R ] (y : R) :

An element y in a monoid is radical if for any element x, y divides x whenever it divides a power of x.

Instances For
theorem zero_isRadical_iff {R : Type u_1} [] :
theorem isRadical_iff_span_singleton {R : Type u_1} {y : R} [] :
theorem isRadical_iff_pow_one_lt {R : Type u_1} {y : R} [] (k : ) (hk : 1 < k) :
∀ (x : R), y x ^ ky x
theorem isReduced_iff_pow_one_lt {R : Type u_1} [] (k : ) (hk : 1 < k) :
∀ (x : R), x ^ k = 0x = 0
theorem Commute.isNilpotent_add {R : Type u_1} {x : R} {y : R} [] (h_comm : Commute x y) (hx : ) (hy : ) :
theorem Commute.isNilpotent_sum {R : Type u_1} [] {ι : Type u_3} {s : } {f : ιR} (hnp : ∀ (i : ι), i sIsNilpotent (f i)) (h_comm : ∀ (i j : ι), i sj sCommute (f i) (f j)) :
IsNilpotent (Finset.sum s fun i => f i)
theorem Commute.isNilpotent_mul_left {R : Type u_1} {x : R} {y : R} [] (h_comm : Commute x y) (h : ) :
theorem Commute.isNilpotent_mul_left_iff {R : Type u_1} {x : R} {y : R} [] (h_comm : Commute x y) (hy : ) :
theorem Commute.isNilpotent_mul_right {R : Type u_1} {x : R} {y : R} [] (h_comm : Commute x y) (h : ) :
theorem Commute.isNilpotent_mul_right_iff {R : Type u_1} {x : R} {y : R} [] (h_comm : Commute x y) (hx : ) :
theorem Commute.isNilpotent_sub {R : Type u_1} {x : R} {y : R} [Ring R] (h_comm : Commute x y) (hx : ) (hy : ) :
theorem isNilpotent_sum {R : Type u_1} [] {ι : Type u_3} {s : } {f : ιR} (hnp : ∀ (i : ι), i sIsNilpotent (f i)) :
IsNilpotent (Finset.sum s fun i => f i)
def nilradical (R : Type u_3) [] :

The nilradical of a commutative semiring is the ideal of nilpotent elements.

Instances For
theorem mem_nilradical {R : Type u_1} [] {x : R} :
x
theorem nilradical_eq_sInf (R : Type u_3) [] :
= sInf {J | }
theorem nilpotent_iff_mem_prime {R : Type u_1} [] {x : R} :
∀ (J : ), x J
theorem nilradical_le_prime {R : Type u_1} [] (J : ) [H : ] :
J
@[simp]
theorem nilradical_eq_zero (R : Type u_3) [] [] :
= 0
@[simp]
theorem LinearMap.isNilpotent_mulLeft_iff (R : Type u_1) {A : Type v} [] [] [Algebra R A] (a : A) :
@[simp]
theorem LinearMap.isNilpotent_mulRight_iff (R : Type u_1) {A : Type v} [] [] [Algebra R A] (a : A) :
@[simp]
theorem LinearMap.isNilpotent_toMatrix_iff {R : Type u_1} [] {ι : Type u_3} {M : Type u_4} [] [] [] [Module R M] (b : Basis ι R M) (f : M →ₗ[R] M) :
IsNilpotent (↑() f)
theorem Module.End.IsNilpotent.mapQ {R : Type u_1} {M : Type v} [Ring R] [] [Module R M] {f : } {p : } (hp : p ) (hnp : ) :