# Nilpotent elements #

This file develops the basic theory of nilpotent elements. In particular it shows that the nilpotent elements are closed under many operations.

For the definition of `nilradical`, see `Mathlib/RingTheory/Nilpotent/Lemmas.lean`.

## Main definitions #

- `isNilpotent_neg_iff`
- `Commute.isNilpotent_add`
- `Commute.isNilpotent_sub`

source
theorem IsNilpotent.neg {R : Type u_1} {x : R} [Ring R] (h : IsNilpotent x) :
IsNilpotent (-x)
source
@[simp]
theorem isNilpotent_neg_iff {R : Type u_1} {x : R} [Ring R] :
IsNilpotent (-x) ↔ IsNilpotent x
source
theorem IsNilpotent.smul {R : Type u_1} {S : Type u_2} [MonoidWithZero R] [MonoidWithZero S] [MulActionWithZero R S] [SMulCommClass R S S] [IsScalarTower R S S] {a : S} (ha : IsNilpotent a) (t : R) :
IsNilpotent (t • a)
source
theorem IsNilpotent.isUnit_sub_one {R : Type u_1} [Ring R] {r : R} (hnil : IsNilpotent r) :
IsUnit (r - 1)
source
theorem IsNilpotent.isUnit_one_sub {R : Type u_1} [Ring R] {r : R} (hnil : IsNilpotent r) :
IsUnit (1 - r)
source
theorem IsNilpotent.isUnit_add_one {R : Type u_1} [Ring R] {r : R} (hnil : IsNilpotent r) :
IsUnit (r + 1)
source
theorem IsNilpotent.isUnit_one_add {R : Type u_1} [Ring R] {r : R} (hnil : IsNilpotent r) :
IsUnit (1 + r)
source
theorem IsNilpotent.isUnit_add_left_of_commute {R : Type u_1} [Ring R] {r u : R} (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) :
IsUnit (u + r)
source
theorem IsNilpotent.isUnit_add_right_of_commute {R : Type u_1} [Ring R] {r u : R} (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) :
IsUnit (r + u)
source
theorem IsUnit.not_isNilpotent {R : Type u_1} [Ring R] [Nontrivial R] {x : R} (hx : IsUnit x) :
¬IsNilpotent x
source
theorem IsNilpotent.not_isUnit {R : Type u_1} [Ring R] [Nontrivial R] {x : R} (hx : IsNilpotent x) :
¬IsUnit x
source
theorem IsIdempotentElem.eq_zero_of_isNilpotent {R : Type u_1} [MonoidWithZero R] {e : R} (idem : IsIdempotentElem e) (nilp : IsNilpotent e) :
e = 0
source
theorem IsNilpotent.eq_zero_of_isIdempotentElem {R : Type u_1} [MonoidWithZero R] {e : R} (idem : IsIdempotentElem e) (nilp : IsNilpotent e) :
e = 0

Alias of `IsIdempotentElem.eq_zero_of_isNilpotent`.

source
instance instIsReducedProd {R : Type u_1} {S : Type u_2} [Zero R] [Pow R ℕ] [Zero S] [Pow S ℕ] [IsReduced R] [IsReduced S] :
IsReduced (R × S)
source
theorem Prime.isRadical {R : Type u_1} [CommMonoidWithZero R] {y : R} (hy : Prime y) :
IsRadical y
source
theorem zero_isRadical_iff {R : Type u_1} [MonoidWithZero R] :
IsRadical 0 ↔ IsReduced R
source
theorem isReduced_iff_pow_one_lt {R : Type u_1} [MonoidWithZero R] (k : ℕ) (hk : 1 < k) :
IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0
source
theorem IsRadical.of_dvd {R : Type u_1} [CancelCommMonoidWithZero R] {x y : R} (hy : IsRadical y) (h0 : y ≠ 0) (hxy : x ∣ y) :
IsRadical x
source
theorem Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) {m n k : ℕ} (hx : x ^ m = 0) (hy : y ^ n = 0) (h : m + n ≤ k + 1) :
(x + y) ^ k = 0
source
theorem Commute.add_pow_add_eq_zero_of_pow_eq_zero {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) {m n : ℕ} (hx : x ^ m = 0) (hy : y ^ n = 0) :
(x + y) ^ (m + n - 1) = 0
source
theorem Commute.isNilpotent_add {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :
IsNilpotent (x + y)
source
theorem Commute.isNilpotent_sum {R : Type u_1} [Semiring R] {ι : Type u_3} {s : Finset ι} {f : ι → R} (hnp : ∀ i ∈ s, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) :
IsNilpotent (∑ i ∈ s, f i)
source
theorem Commute.isNilpotent_finsum {R : Type u_1} [Semiring R] {ι : Type u_3} {f : ι → R} (hf : ∀ (b : ι), IsNilpotent (f b)) (h_comm : ∀ (i j : ι), Commute (f i) (f j)) :
IsNilpotent (finsum f)
source
theorem Commute.isNilpotent_mul_right_iff {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) (hy : y ∈ nonZeroDivisorsRight R) :
IsNilpotent (x * y) ↔ IsNilpotent x
source
theorem Commute.isNilpotent_mul_left_iff {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) (hx : x ∈ nonZeroDivisorsLeft R) :
IsNilpotent (x * y) ↔ IsNilpotent y
source
theorem Commute.isNilpotent_sub {R : Type u_1} {x y : R} [Ring R] (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :
IsNilpotent (x - y)
source
theorem isNilpotent_sum {R : Type u_1} [CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → R} (hnp : ∀ i ∈ s, IsNilpotent (f i)) :
IsNilpotent (∑ i ∈ s, f i)
source
theorem isNilpotent_finsum {R : Type u_1} [CommSemiring R] {ι : Type u_3} {f : ι → R} (hf : ∀ (b : ι), IsNilpotent (f b)) :
IsNilpotent (finsum f)
source
theorem NoZeroSMulDivisors.isReduced (R : Type u_3) (M : Type u_4) [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Nontrivial M] [NoZeroSMulDivisors R M] :
IsReduced R