Documentation

Mathlib.RingTheory.Nilpotent.Defs

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 #

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