Documentation

Mathlib.RingTheory.Nilpotent.Basic

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 #

theorem IsNilpotent.neg {R : Type u_1} {x : R} [Ring R] (h : IsNilpotent x) :

IsNilpotent (-x)

@[simp]

theorem isNilpotent_neg_iff {R : Type u_1} {x : R} [Ring R] :

IsNilpotent (-x) ↔ IsNilpotent x

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)

theorem IsNilpotent.isUnit_sub_one {R : Type u_1} [Ring R] {r : R} (hnil : IsNilpotent r) :

IsUnit (r - 1)

theorem IsNilpotent.isUnit_one_sub {R : Type u_1} [Ring R] {r : R} (hnil : IsNilpotent r) :

IsUnit (1 - r)

theorem IsNilpotent.isUnit_add_one {R : Type u_1} [Ring R] {r : R} (hnil : IsNilpotent r) :

IsUnit (r + 1)

theorem IsNilpotent.isUnit_one_add {R : Type u_1} [Ring R] {r : R} (hnil : IsNilpotent r) :

IsUnit (1 + r)

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)

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)

theorem IsUnit.not_isNilpotent {R : Type u_1} [Ring R] [Nontrivial R] {x : R} (hx : IsUnit x) :

¬IsNilpotent x

theorem IsNilpotent.not_isUnit {R : Type u_1} [Ring R] [Nontrivial R] {x : R} (hx : IsNilpotent x) :

theorem IsIdempotentElem.eq_zero_of_isNilpotent {R : Type u_1} [MonoidWithZero R] {e : R} (idem : IsIdempotentElem e) (nilp : IsNilpotent e) :

e = 0

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.

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)

theorem Prime.isRadical {R : Type u_1} [CommMonoidWithZero R] {y : R} (hy : Prime y) :

theorem zero_isRadical_iff {R : Type u_1} [MonoidWithZero R] :

IsRadical 0 ↔ IsReduced R

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

theorem IsRadical.of_dvd {R : Type u_1} [CancelCommMonoidWithZero R] {x y : R} (hy : IsRadical y) (h0 : y ≠ 0) (hxy : x ∣ y) :

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

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

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)

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)

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)

theorem Commute.isNilpotent_mul_left_iff {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) (hy : y ∈ nonZeroDivisorsLeft R) :

IsNilpotent (x * y) ↔ IsNilpotent x

theorem Commute.isNilpotent_mul_right_iff {R : Type u_1} {x y : R} [Semiring R] (h_comm : Commute x y) (hx : x ∈ nonZeroDivisorsRight R) :

IsNilpotent (x * y) ↔ IsNilpotent y

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)

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)

theorem isNilpotent_finsum {R : Type u_1} [CommSemiring R] {ι : Type u_3} {f : ι → R} (hf : ∀ (b : ι), IsNilpotent (f b)) :

IsNilpotent (finsum f)

theorem NoZeroSMulDivisors.isReduced (R : Type u_3) (M : Type u_4) [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Nontrivial M] [NoZeroSMulDivisors R M] :