# Definition of nilpotent elements #

This file defines the notion of a nilpotent element and proves the immediate consequences. For results that require further theory, see `Mathlib/RingTheory/Nilpotent/Basic.lean` and `Mathlib/RingTheory/Nilpotent/Lemmas.lean`.

## Main definitions #

- `IsNilpotent`
- `Commute.isNilpotent_mul_left`
- `Commute.isNilpotent_mul_right`
- `nilpotencyClass`

source
def IsNilpotent {R : Type u_1} [Zero R] [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 `MonoidWithZero` is too strong since nilpotency is important in the study of rings that are only power-associative.

Equations

- IsNilpotent x = ∃ (n : ℕ), x ^ n = 0

Instances For

source
theorem IsNilpotent.mk {R : Type u_1} [Zero R] [Pow R ℕ] (x : R) (n : ℕ) (e : x ^ n = 0) :
IsNilpotent x
source
@[simp]
theorem isNilpotent_of_subsingleton {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [Subsingleton R] :
IsNilpotent x
source
@[simp]
theorem IsNilpotent.zero {R : Type u_1} [MonoidWithZero R] :
IsNilpotent 0
source
theorem not_isNilpotent_one {R : Type u_1} [MonoidWithZero R] [Nontrivial R] :
¬IsNilpotent 1
source
theorem IsNilpotent.pow_succ (n : ℕ) {S : Type u_3} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) :
IsNilpotent (x ^ n.succ)
source
theorem IsNilpotent.of_pow {R : Type u_1} [MonoidWithZero R] {x : R} {m : ℕ} (h : IsNilpotent (x ^ m)) :
IsNilpotent x
source
theorem IsNilpotent.pow_of_pos {n : ℕ} {S : Type u_3} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) (hn : n ≠ 0) :
IsNilpotent (x ^ n)
source
@[simp]
theorem IsNilpotent.pow_iff_pos {n : ℕ} {S : Type u_3} [MonoidWithZero S] {x : S} (hn : n ≠ 0) :
IsNilpotent (x ^ n) ↔ IsNilpotent x
source
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)
source
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
source
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
source
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
source
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`.

Equations

- nilpotencyClass x = sInf {k : ℕ | x ^ k = 0}

Instances For

source
@[simp]
theorem nilpotencyClass_eq_zero_of_subsingleton {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [Subsingleton R] :
nilpotencyClass x = 0
source
theorem isNilpotent_of_pos_nilpotencyClass {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] (hx : 0 < nilpotencyClass x) :
IsNilpotent x
source
theorem pow_nilpotencyClass {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] (hx : IsNilpotent x) :
x ^ nilpotencyClass x = 0
source
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
source
@[simp]
theorem nilpotencyClass_zero {R : Type u_1} [MonoidWithZero R] [Nontrivial R] :
nilpotencyClass 0 = 1
source
@[simp]
theorem pos_nilpotencyClass_iff {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] :
0 < nilpotencyClass x ↔ IsNilpotent x
source
theorem pow_pred_nilpotencyClass {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] (hx : IsNilpotent x) :
x ^ (nilpotencyClass x - 1) ≠ 0
source
theorem eq_zero_of_nilpotencyClass_eq_one {R : Type u_1} {x : R} [MonoidWithZero R] (hx : nilpotencyClass x = 1) :
x = 0
source
@[simp]
theorem nilpotencyClass_eq_one {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] :
nilpotencyClass x = 1 ↔ x = 0
source
class IsReduced (R : Type u_3) [Zero R] [Pow R ℕ] :
Prop

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

- eq_zero (x : R) : IsNilpotent x → x = 0

  A reduced structure has no nonzero nilpotent elements.

Instances

source
theorem isReduced_iff (R : Type u_3) [Zero R] [Pow R ℕ] :
IsReduced R ↔ ∀ (x : R), IsNilpotent x → x = 0
source
theorem IsReduced.pow_eq_zero {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] {n : ℕ} (h : x ^ n = 0) :
x = 0
source
@[simp]
theorem IsReduced.pow_eq_zero_iff {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) :
x ^ n = 0 ↔ x = 0
source
theorem IsReduced.pow_ne_zero_iff {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) :
x ^ n ≠ 0 ↔ x ≠ 0
source
theorem IsReduced.pow_ne_zero {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] (n : ℕ) (h : x ≠ 0) :
x ^ n ≠ 0
source
@[simp]
theorem IsReduced.pow_eq_zero_iff' {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] [Nontrivial R] {n : ℕ} :
x ^ n = 0 ↔ x = 0 ∧ n ≠ 0

A variant of `IsReduced.pow_eq_zero_iff` assuming `R` is not trivial.

source
@[instance 900]
instance isReduced_of_noZeroDivisors {R : Type u_1} [MonoidWithZero R] [NoZeroDivisors R] :
IsReduced R
source
@[instance 900]
instance isReduced_of_subsingleton {R : Type u_1} [Zero R] [Pow R ℕ] [Subsingleton R] :
IsReduced R
source
theorem IsNilpotent.eq_zero {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [IsReduced R] (h : IsNilpotent x) :
x = 0
source
@[simp]
theorem isNilpotent_iff_eq_zero {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] :
IsNilpotent x ↔ x = 0
source
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
source
theorem exists_isNilpotent_of_not_isReduced {R : Type u_3} [Zero R] [Pow R ℕ] (h : ¬IsReduced R) :
∃ (x : R), x ≠ 0 ∧ IsNilpotent x
source
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)
source
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`.

Equations

- IsRadical y = ∀ (n : ℕ) (x : R), y ∣ x ^ n → y ∣ x

Instances For

source
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
source
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)
source
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)