Documentation

Mathlib.RingTheory.Nilpotent.Defs

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 and Mathlib.RingTheory.Nilpotent.Lemmas.

Main definitions #

def IsNilpotent {R : Type u_1} [Zero R] [Pow R ] (x : R) :

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
Instances For
    theorem IsNilpotent.mk {R : Type u_1} [Zero R] [Pow R ] (x : R) (n : ) (e : x ^ n = 0) :
    @[simp]
    theorem isNilpotent_of_subsingleton {R : Type u_1} {x : R} [Zero R] [Pow R ] [Subsingleton R] :
    @[simp]
    theorem IsNilpotent.pow_succ (n : ) {S : Type u_3} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) :
    IsNilpotent (x ^ n.succ)
    theorem IsNilpotent.of_pow {R : Type u_1} [MonoidWithZero R] {x : R} {m : } (h : IsNilpotent (x ^ m)) :
    theorem IsNilpotent.pow_of_pos {n : } {S : Type u_3} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) (hn : n 0) :
    @[simp]
    theorem IsNilpotent.pow_iff_pos {n : } {S : Type u_3} [MonoidWithZero S] {x : S} (hn : n 0) :
    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) :
    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) :
    theorem IsUnit.isNilpotent_mul_unit_of_commute_iff {R : Type u_1} [MonoidWithZero R] {r : R} {u : R} (hu : IsUnit u) (h_comm : Commute r u) :
    theorem IsUnit.isNilpotent_unit_mul_of_commute_iff {R : Type u_1} [MonoidWithZero R] {r : R} {u : R} (hu : IsUnit u) (h_comm : Commute r u) :
    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
      @[simp]
      theorem isNilpotent_of_pos_nilpotencyClass {R : Type u_1} {x : R} [Zero R] [Pow R ] (hx : 0 < nilpotencyClass x) :
      theorem pow_nilpotencyClass {R : Type u_1} {x : R} [Zero R] [Pow R ] (hx : IsNilpotent x) :
      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
      theorem pow_pred_nilpotencyClass {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] (hx : IsNilpotent x) :
      theorem eq_zero_of_nilpotencyClass_eq_one {R : Type u_1} {x : R} [MonoidWithZero R] (hx : nilpotencyClass x = 1) :
      x = 0
      @[simp]
      theorem nilpotencyClass_eq_one {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] :
      theorem isReduced_iff (R : Type u_3) [Zero R] [Pow R ] :
      IsReduced R ∀ (x : R), IsNilpotent xx = 0
      class IsReduced (R : Type u_3) [Zero R] [Pow R ] :

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

      • eq_zero : ∀ (x : R), IsNilpotent xx = 0

        A reduced structure has no nonzero nilpotent elements.

      Instances
        theorem IsReduced.eq_zero {R : Type u_3} :
        ∀ {inst : Zero R} {inst_1 : Pow R } [self : IsReduced R] (x : R), IsNilpotent xx = 0

        A reduced structure has no nonzero nilpotent elements.

        theorem IsReduced.pow_eq_zero {R : Type u_1} {x : R} [Zero R] [Pow R ] [IsReduced R] {n : } (h : x ^ n = 0) :
        x = 0
        @[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
        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
        theorem IsReduced.pow_ne_zero {R : Type u_1} {x : R} [Zero R] [Pow R ] [IsReduced R] (n : ) (h : x 0) :
        x ^ n 0
        @[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.

        @[instance 900]
        Equations
        • =
        @[instance 900]
        instance isReduced_of_subsingleton {R : Type u_1} [Zero R] [Pow R ] [Subsingleton R] :
        Equations
        • =
        theorem IsNilpotent.eq_zero {R : Type u_1} {x : R} [Zero R] [Pow R ] [IsReduced R] (h : IsNilpotent x) :
        x = 0
        @[simp]
        theorem isNilpotent_iff_eq_zero {R : Type u_1} {x : R} [MonoidWithZero R] [IsReduced R] :
        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] :
        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)
        Equations
        • =
        def IsRadical {R : Type u_1} [Dvd R] [Pow R ] (y : R) :

        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
          theorem isRadical_iff_pow_one_lt {R : Type u_1} {y : R} [MonoidWithZero R] (k : ) (hk : 1 < k) :
          IsRadical y ∀ (x : R), y x ^ ky x
          theorem Commute.isNilpotent_mul_left {R : Type u_1} {x : R} {y : R} [Semiring R] (h_comm : Commute x y) (h : IsNilpotent x) :
          theorem Commute.isNilpotent_mul_right {R : Type u_1} {x : R} {y : R} [Semiring R] (h_comm : Commute x y) (h : IsNilpotent y) :