# mathlib3documentation

ring_theory.nilpotent

# Nilpotent elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• is_nilpotent
• is_nilpotent_neg_iff
• commute.is_nilpotent_add
• commute.is_nilpotent_mul_left
• commute.is_nilpotent_mul_right
• commute.is_nilpotent_sub
def is_nilpotent {R : Type u} [has_zero R] [ ] (x : R) :
Prop

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 monoid_with_zero is too strong since nilpotency is important in the study of rings that are only power-associative.

Equations
theorem is_nilpotent.mk {R : Type u} [has_zero R] [ ] (x : R) (n : ) (e : x ^ n = 0) :
theorem is_nilpotent.zero {R : Type u}  :
theorem is_nilpotent.neg {R : Type u} {x : R} [ring R] (h : is_nilpotent x) :
@[simp]
theorem is_nilpotent_neg_iff {R : Type u} {x : R} [ring R] :
theorem is_nilpotent.map {R S : Type u} {r : R} {F : Type u_1} [ S] (hr : is_nilpotent r) (f : F) :
theorem is_reduced_iff (R : Type u_1) [has_zero R] [ ] :
(x : R), x = 0
@[class]
structure is_reduced (R : Type u_1) [has_zero R] [ ] :
Prop

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]
theorem is_nilpotent.eq_zero {R : Type u} {x : R} [has_zero R] [ ] [is_reduced R] (h : is_nilpotent x) :
x = 0
@[simp]
theorem is_nilpotent_iff_eq_zero {R : Type u} {x : R} [is_reduced R] :
x = 0
theorem is_reduced_of_injective {R S : Type u} {F : Type u_1} [ S] (f : F) (hf : function.injective f) [is_reduced S] :
theorem ring_hom.ker_is_radical_iff_reduced_of_surjective {R : Type u} {S : Type u_1} {F : Type u_2} [comm_ring S] [ S] {f : F} (hf : function.surjective f) :
def is_radical {R : Type u} [has_dvd R] [ ] (y : R) :
Prop

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

Equations
theorem zero_is_radical_iff {R : Type u}  :
theorem is_radical_iff_pow_one_lt {R : Type u} {y : R} (k : ) (hk : 1 < k) :
(x : R), y x ^ k y x
theorem is_reduced_iff_pow_one_lt {R : Type u} (k : ) (hk : 1 < k) :
(x : R), x ^ k = 0 x = 0
theorem commute.is_nilpotent_add {R : Type u} {x y : R} [semiring R] (h_comm : y) (hx : is_nilpotent x) (hy : is_nilpotent y) :
theorem commute.is_nilpotent_mul_left {R : Type u} {x y : R} [semiring R] (h_comm : y) (h : is_nilpotent x) :
theorem commute.is_nilpotent_mul_right {R : Type u} {x y : R} [semiring R] (h_comm : y) (h : is_nilpotent y) :
theorem commute.is_nilpotent_sub {R : Type u} {x y : R} [ring R] (h_comm : y) (hx : is_nilpotent x) (hy : is_nilpotent y) :
def nilradical (R : Type u_1)  :

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

Equations
theorem mem_nilradical {R : Type u} {x : R}  :
x
theorem nilradical_eq_Inf (R : Type u_1)  :
theorem nilpotent_iff_mem_prime {R : Type u} {x : R}  :
(J : ideal R), J.is_prime x J
theorem nilradical_le_prime {R : Type u} (J : ideal R) [H : J.is_prime] :
J
@[simp]
theorem nilradical_eq_zero (R : Type u_1) [is_reduced R] :
= 0
@[simp]
theorem linear_map.is_nilpotent_mul_left_iff (R : Type u) {A : Type v} [semiring A] [ A] (a : A) :
@[simp]
theorem linear_map.is_nilpotent_mul_right_iff (R : Type u) {A : Type v} [semiring A] [ A] (a : A) :
theorem module.End.is_nilpotent.mapq {R : Type u} {M : Type v} [ring R] [ M] {f : M} {p : M} (hp : p ) (hnp : is_nilpotent f) :
is_nilpotent (p.mapq p f hp)