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.mk {R : Type u} [has_zero R] [has_pow R ] (x : R) (n : ) (e : x ^ n = 0) :
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} [monoid_with_zero R] [monoid_with_zero S] {r : R} {F : Type u_1} [monoid_with_zero_hom_class F R S] (hr : is_nilpotent r) (f : F) :
theorem is_reduced_iff (R : Type u_1) [has_zero R] [has_pow R ] :
is_reduced R (x : R), is_nilpotent x x = 0
@[class]
structure is_reduced (R : Type u_1) [has_zero R] [has_pow 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] [has_pow R ] [is_reduced R] (h : is_nilpotent x) :
x = 0
@[simp]
theorem is_nilpotent_iff_eq_zero {R : Type u} {x : R} [monoid_with_zero R] [is_reduced R] :
def is_radical {R : Type u} [has_dvd R] [has_pow 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 is_radical_iff_pow_one_lt {R : Type u} {y : R} [monoid_with_zero R] (k : ) (hk : 1 < k) :
is_radical y (x : R), y x ^ k y x
theorem is_reduced_iff_pow_one_lt {R : Type u} [monoid_with_zero R] (k : ) (hk : 1 < k) :
is_reduced R (x : R), x ^ k = 0 x = 0
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) :
def nilradical (R : Type u_1) [comm_semiring R] :

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

Equations
theorem mem_nilradical {R : Type u} {x : R} [comm_semiring R] :
theorem nilpotent_iff_mem_prime {R : Type u} {x : R} [comm_semiring R] :
theorem nilradical_le_prime {R : Type u} [comm_semiring R] (J : ideal R) [H : J.is_prime] :
@[simp]
theorem nilradical_eq_zero (R : Type u_1) [comm_semiring R] [is_reduced R] :
theorem module.End.is_nilpotent.mapq {R : Type u} {M : Type v} [ring R] [add_comm_group M] [module R M] {f : module.End R M} {p : submodule R M} (hp : p submodule.comap f 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 : comm_ring S], ideal S Prop} (h₁ : ⦃S : Type u⦄ [_inst_5 : comm_ring S] (I : ideal S), I ^ 2 = P I) (h₂ : ⦃S : Type u⦄ [_inst_6 : comm_ring S] (I J : ideal S), I J P I P (ideal.map (ideal.quotient.mk I) 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.