Definition of nilpotent elements

This file proves basic facts about nilpotent elements. For results that require further theory, see Mathlib/RingTheory/Nilpotent/Basic.lean and Mathlib/RingTheory/Nilpotent/Lemmas.lean.

Main definitions

• Commute.isNilpotent_mul_left
• Commute.isNilpotent_mul_right
• nilpotencyClass

theorem IsNilpotent.map {R : Type u_1} {S : Type u_2} [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type u_3} [FunLike F R S] [MonoidWithZeroHomClass F R S] (hr : IsNilpotent r) (f : F) : IsNilpotent (f r)

theorem IsNilpotent.map_iff {R : Type u_1} {S : Type u_2} [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type u_3} [FunLike F R S] [MonoidWithZeroHomClass F R S] {f : F} (hf : Function.Injective ⇑f) : IsNilpotent (f r) ↔ IsNilpotent r

theorem IsUnit.isNilpotent_mul_unit_of_commute_iff {R : Type u_1} [MonoidWithZero R] {r u : R} (hu : IsUnit u) (h_comm : Commute r u) : IsNilpotent (r * u) ↔ IsNilpotent r

theorem IsUnit.isNilpotent_unit_mul_of_commute_iff {R : Type u_1} [MonoidWithZero R] {r u : R} (hu : IsUnit u) (h_comm : Commute r u) : IsNilpotent (u * r) ↔ IsNilpotent r

noncomputable def nilpotencyClass {R : Type u_1} (x : R) [Zero R] [Pow R ℕ] : ℕ

If x is nilpotent, the nilpotency class is the smallest natural number k such that x ^ k = 0. If x is not nilpotent, the nilpotency class takes the junk value 0.

@[simp]

theorem nilpotencyClass_eq_zero_of_subsingleton {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [Subsingleton R] : nilpotencyClass x = 0

theorem isNilpotent_of_pos_nilpotencyClass {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] (hx : 0 < nilpotencyClass x) : IsNilpotent x

theorem pow_nilpotencyClass {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] (hx : IsNilpotent x) : x ^ nilpotencyClass x = 0

theorem nilpotencyClass_eq_succ_iff {R : Type u_1} {x : R} [MonoidWithZero R] {k : ℕ} : nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

@[simp]

theorem nilpotencyClass_zero {R : Type u_1} [MonoidWithZero R] [Nontrivial R] : nilpotencyClass 0 = 1

@[simp]

theorem pos_nilpotencyClass_iff {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] : 0 < nilpotencyClass x ↔ IsNilpotent x

theorem pow_pred_nilpotencyClass {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] (hx : IsNilpotent x) : x ^ (nilpotencyClass x - 1) ≠ 0

theorem eq_zero_of_nilpotencyClass_eq_one {R : Type u_1} {x : R} [MonoidWithZero R] (hx : nilpotencyClass x = 1) : x = 0

@[simp]

theorem nilpotencyClass_eq_one {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] : nilpotencyClass x = 1 ↔ x = 0

theorem isReduced_of_injective {R : Type u_1} {S : Type u_2} [MonoidWithZero R] [MonoidWithZero S] {F : Type u_3} [FunLike F R S] [MonoidWithZeroHomClass F R S] (f : F) (hf : Function.Injective ⇑f) [IsReduced S] : IsReduced R

instance instIsReducedForall (ι : Type u_4) (R : ι → Type u_3) [(i : ι) → Zero (R i)] [(i : ι) → Pow (R i) ℕ] [∀ (i : ι), IsReduced (R i)] : IsReduced ((i : ι) → R i)

def IsRadical {R : Type u_1} [Dvd R] [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.

theorem isRadical_iff_pow_one_lt {R : Type u_1} {y : R} [Monoid R] (k : ℕ) (hk : 1 < k) : IsRadical y ↔ ∀ (x : R), y ∣ x ^ k → y ∣ x

theorem Commute.isNilpotent_mul_right {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) (h : IsNilpotent x) : IsNilpotent (x * y)

theorem Commute.isNilpotent_mul_left {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) (h : IsNilpotent y) : IsNilpotent (x * y)