Documentation

Mathlib.RingTheory.Nilpotent.Lemmas

Nilpotent elements #

This file contains results about nilpotent elements that involve ring theory.

theorem RingHom.ker_isRadical_iff_reduced_of_surjective {R : Type u_1} {S : Type u_3} {F : Type u_4} [CommSemiring R] [CommRing S] [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective f) :
(RingHom.ker f).IsRadical IsReduced S
theorem isRadical_iff_span_singleton {R : Type u_1} {y : R} [CommSemiring R] :
IsRadical y (Ideal.span {y}).IsRadical
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 nilradical_eq_sInf (R : Type u_3) [CommSemiring R] :
    nilradical R = sInf {J : Ideal R | J.IsPrime}
    theorem nilpotent_iff_mem_prime {R : Type u_1} [CommSemiring R] {x : R} :
    IsNilpotent x ∀ (J : Ideal R), J.IsPrimex J
    theorem nilradical_le_prime {R : Type u_1} [CommSemiring R] (J : Ideal R) [H : J.IsPrime] :
    @[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_restrict_of_le {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} {p : Submodule R M} {q : Submodule R M} {hp : Set.MapsTo f p p} {hq : Set.MapsTo f q q} (h : p q) (hf : IsNilpotent (LinearMap.restrict f hq)) :
    theorem Module.End.isNilpotent.restrict {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] M} {p : Submodule R M} (hf : Set.MapsTo f p p) (hnil : IsNilpotent f) :
    IsNilpotent (f.restrict hf)
    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) :
    IsNilpotent (p.mapQ p f hp)