mathlib documentation

ring_theory.nilpotent

Nilpotent elements #

Main definitions #

def is_nilpotent {R : Type u} [has_zero R] [has_pow 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.zero {R : Type u} [monoid_with_zero R] :
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.eq_zero {R : Type u} {x : R} [monoid_with_zero R] [no_zero_divisors R] (h : is_nilpotent x) :
x = 0
@[simp]
theorem is_nilpotent_iff_eq_zero {R : Type u} {x : R} [monoid_with_zero R] [no_zero_divisors R] :
theorem commute.is_nilpotent_add {R : Type u} {x y : R} [semiring R] (h_comm : commute x 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 : commute x y) (h : is_nilpotent x) :
theorem commute.is_nilpotent_mul_right {R : Type u} {x y : R} [semiring R] (h_comm : commute x y) (h : is_nilpotent y) :
theorem commute.is_nilpotent_sub {R : Type u} {x y : R} [ring R] (h_comm : commute x y) (hx : is_nilpotent x) (hy : is_nilpotent y) :
@[simp]
theorem algebra.is_nilpotent_lmul_left_iff (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
@[simp]
theorem algebra.is_nilpotent_lmul_right_iff (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :