Documentation

Mathlib.RingTheory.Nilpotent

Nilpotent elements #

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.neg {R : Type u_1} {x : R} [Ring R] (h : IsNilpotent x) :
    theorem IsNilpotent.pow_succ (n : ) {S : Type u_3} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) :
    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) :
    @[simp]
    theorem isNilpotent_neg_iff {R : Type u_1} {x : R} [Ring R] :
    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) :
    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) :
    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 : 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 : R} {u : R} (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) :
    IsUnit (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
        Equations
        • =
        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 instIsReducedProdInstZeroPowNat {R : Type u_1} {S : Type u_2} [Zero R] [Pow R ] [Zero S] [Pow S ] [IsReduced R] [IsReduced S] :
        Equations
        • =
        instance instIsReducedForAllInstZeroInstPowNat (ι : 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 Prime.isRadical {R : Type u_1} [CommMonoidWithZero R] {y : R} (hy : Prime y) :
          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 isReduced_iff_pow_one_lt {R : Type u_1} [MonoidWithZero R] (k : ) (hk : 1 < k) :
          IsReduced R ∀ (x : R), x ^ k = 0x = 0
          theorem IsRadical.of_dvd {R : Type u_1} [CancelCommMonoidWithZero R] {x : R} {y : R} (hy : IsRadical y) (h0 : y 0) (hxy : x y) :
          theorem Commute.isNilpotent_add {R : Type u_1} {x : R} {y : R} [Semiring R] (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :
          theorem Commute.isNilpotent_sum {R : Type u_1} [Semiring R] {ι : Type u_3} {s : Finset ι} {f : ιR} (hnp : is, IsNilpotent (f i)) (h_comm : ∀ (i j : ι), i sj sCommute (f i) (f j)) :
          IsNilpotent (Finset.sum s fun (i : ι) => f i)
          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_left_iff {R : Type u_1} {x : R} {y : R} [Semiring R] (h_comm : Commute x y) (hy : y nonZeroDivisorsLeft R) :
          theorem Commute.isNilpotent_mul_right {R : Type u_1} {x : R} {y : R} [Semiring R] (h_comm : Commute x y) (h : IsNilpotent y) :
          theorem Commute.isNilpotent_mul_right_iff {R : Type u_1} {x : R} {y : R} [Semiring R] (h_comm : Commute x y) (hx : x nonZeroDivisorsRight R) :
          theorem Commute.isNilpotent_sub {R : Type u_1} {x : R} {y : R} [Ring R] (h_comm : Commute x y) (hx : IsNilpotent x) (hy : IsNilpotent y) :
          theorem isNilpotent_sum {R : Type u_1} [CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ιR} (hnp : is, IsNilpotent (f i)) :
          IsNilpotent (Finset.sum s fun (i : ι) => f i)
          def nilradical (R : Type u_3) [CommSemiring R] :

          The nilradical of a commutative semiring is the ideal of nilpotent elements.

          Equations
          Instances For
            theorem mem_nilradical {R : Type u_1} [CommSemiring R] {x : R} :
            theorem nilpotent_iff_mem_prime {R : Type u_1} [CommSemiring R] {x : R} :
            IsNilpotent x ∀ (J : Ideal R), Ideal.IsPrime Jx J
            theorem nilradical_le_prime {R : Type u_1} [CommSemiring R] (J : Ideal R) [H : Ideal.IsPrime J] :
            @[simp]
            theorem nilradical_eq_zero (R : Type u_3) [CommSemiring R] [IsReduced R] :
            @[simp]
            theorem LinearMap.isNilpotent_toMatrix_iff {R : Type u_1} [CommSemiring R] {ι : Type u_3} {M : Type u_4} [Fintype ι] [DecidableEq ι] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (f : M →ₗ[R] M) :
            theorem Module.End.IsNilpotent.mapQ {R : Type u_1} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] {f : Module.End R M} {p : Submodule R M} (hp : p Submodule.comap f p) (hnp : IsNilpotent f) :