mathlib documentation


Nilpotent elements #

Main definitions #

def is_nilpotent {R : Type u} [has_zero R] [has_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 monoid_with_zero is too strong since nilpotency is important in the study of rings that are only power-associative.

theorem {R : Type u} [has_zero R] [has_pow R ] (x : R) (n : ) (e : x ^ n = 0) :
theorem {R : Type u} [monoid_with_zero R] :
theorem is_nilpotent.neg {R : Type u} {x : R} [ring R] (h : is_nilpotent x) :
theorem is_nilpotent_neg_iff {R : Type u} {x : R} [ring R] :
theorem {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) :
structure is_reduced (R : Type u_1) [has_zero R] [has_pow R ] :

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
theorem is_nilpotent_iff_eq_zero {R : Type u} {x : R} [monoid_with_zero R] [is_reduced R] :
theorem is_reduced_of_injective {R S : Type u} [monoid_with_zero R] [monoid_with_zero S] {F : Type u_1} [monoid_with_zero_hom_class F R 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 : 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.

theorem mem_nilradical {R : Type u} {x : R} [comm_semiring R] :
theorem nilradical_eq_Inf (R : Type u_1) [comm_semiring R] :
theorem nilpotent_iff_mem_prime {R : Type u} {x : R} [comm_semiring R] :
is_nilpotent x ∀ (J : ideal R), J.is_primex J
theorem nilradical_le_prime {R : Type u} [comm_semiring R] (J : ideal R) [H : J.is_prime] :
theorem nilradical_eq_zero (R : Type u_1) [comm_semiring R] [is_reduced R] :
theorem linear_map.is_nilpotent_mul_left_iff (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
theorem linear_map.is_nilpotent_mul_right_iff (R : Type u) {A : Type v} [comm_semiring R] [semiring A] [algebra R A] (a : A) :
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 JP IP ( ( I) J)P J) :

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} :