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.

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