# mathlibdocumentation

ring_theory.nilpotent

# Nilpotent elements #

## 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) :
@[class]
structure is_reduced (R : Type u_1) [has_zero R] [ ] :
Prop
• eq_zero : ∀ (x : R), x = 0

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

Instances of this typeclass
@[protected, instance]
def is_reduced_of_no_zero_divisors {R : Type u}  :
@[protected, instance]
def is_reduced_of_subsingleton {R : Type u} [has_zero R] [ ] [subsingleton R] :
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 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_primex 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)
theorem ideal.is_nilpotent.induction_on {S : Type u} [comm_ring S] (I : ideal S) (hI : is_nilpotent I) {P : Π ⦃S : Type u⦄ [_inst_4 : , → Prop} (h₁ : ∀ ⦃S : Type u⦄ [_inst_5 : (I : ideal S), I ^ 2 = P I) (h₂ : ∀ ⦃S : Type u⦄ [_inst_6 : (I J : ideal S), I JP IP J)P J) :
P I

Let P be a property on ideals. If P holds for square-zero ideals, and if P I → P (J ⧸ I) → P J, then P holds for all nilpotent ideals.

theorem is_nilpotent.is_unit_quotient_mk_iff {R : Type u_1} [comm_ring R] {I : ideal R} (hI : is_nilpotent I) {x : R} :