Documentation

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.zero {R : Type u_1} [MonoidWithZero R] :

IsNilpotent 0

theorem not_isNilpotent_one {R : Type u_1} [MonoidWithZero R] [Nontrivial R] :

¬IsNilpotent 1

theorem IsNilpotent.neg {R : Type u_1} {x : R} [Ring R] (h : IsNilpotent x) :

IsNilpotent (-x)

theorem IsNilpotent.pow_succ (n : ℕ) {S : Type u_3} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) :

IsNilpotent (x ^ Nat.succ n)

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

IsNilpotent (x ^ n)

@[simp]

theorem IsNilpotent.pow_iff_pos {n : ℕ} {S : Type u_3} [MonoidWithZero S] {x : S} (hn : n ≠ 0) :

IsNilpotent (x ^ n) ↔ 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.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)

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

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

IsNilpotent (r * u) ↔ IsNilpotent r

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

IsNilpotent (u * r) ↔ IsNilpotent r

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

nilpotencyClass x = sInf {k : ℕ | x ^ k = 0}

Instances For

@[simp]

theorem nilpotencyClass_eq_zero_of_subsingleton {R : Type u_1} {x : R} [Zero R] [Pow R ℕ] [Subsingleton R] :

nilpotencyClass x = 0

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

x ^ nilpotencyClass x = 0

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

@[simp]

theorem nilpotencyClass_zero {R : Type u_1} [MonoidWithZero R] [Nontrivial R] :

nilpotencyClass 0 = 1

@[simp]

theorem pos_nilpotencyClass_iff {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] :

0 < nilpotencyClass x ↔ IsNilpotent x

theorem pow_pred_nilpotencyClass {R : Type u_1} {x : R} [MonoidWithZero R] [Nontrivial R] (hx : IsNilpotent x) :

x ^ (nilpotencyClass x - 1) ≠ 0

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

nilpotencyClass x = 1 ↔ x = 0

theorem isReduced_iff (R : Type u_3) [Zero R] [Pow R ℕ] :

IsReduced R ↔ ∀ (x : R), IsNilpotent x → x = 0

class IsReduced (R : Type u_3) [Zero R] [Pow R ℕ] :

Prop

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

eq_zero : ∀ (x : R), IsNilpotent x → x = 0
A reduced structure has no nonzero nilpotent elements.

Instances

instance isReduced_of_noZeroDivisors {R : Type u_1} [MonoidWithZero R] [NoZeroDivisors R] :

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

IsNilpotent x ↔ x = 0

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

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

Ideal.IsRadical (RingHom.ker 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] :

IsReduced (R × 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) :

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

IsRadical y = ∀ (n : ℕ) (x : R), y ∣ x ^ n → y ∣ x

Instances For

theorem Prime.isRadical {R : Type u_1} [CommMonoidWithZero R] {y : R} (hy : Prime y) :

IsRadical y

theorem zero_isRadical_iff {R : Type u_1} [MonoidWithZero R] :

IsRadical 0 ↔ IsReduced R

theorem isRadical_iff_span_singleton {R : Type u_1} {y : R} [CommSemiring R] :

IsRadical y ↔ Ideal.IsRadical (Ideal.span {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 ^ k → y ∣ x

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 : R} {y : R} (hy : IsRadical y) (h0 : y ≠ 0) (hxy : x ∣ y) :

IsRadical x

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

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

IsNilpotent (x * y)

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

IsNilpotent (x * y) ↔ 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) :

IsNilpotent (x * 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) :

IsNilpotent (x * y) ↔ IsNilpotent y

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

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 (Finset.sum s fun (i : ι) => f i)

def nilradical (R : Type u_3) [CommSemiring R] :

Ideal R

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

Equations

nilradical R = Ideal.radical 0

Instances For

theorem mem_nilradical {R : Type u_1} [CommSemiring R] {x : R} :

x ∈ nilradical R ↔ IsNilpotent x

theorem nilradical_eq_sInf (R : Type u_3) [CommSemiring R] :

nilradical R = sInf {J : Ideal R | Ideal.IsPrime J}

theorem nilpotent_iff_mem_prime {R : Type u_1} [CommSemiring R] {x : R} :

IsNilpotent x ↔ ∀ (J : Ideal R), Ideal.IsPrime J → x ∈ J

theorem nilradical_le_prime {R : Type u_1} [CommSemiring R] (J : Ideal R) [H : Ideal.IsPrime J] :

nilradical R ≤ J

@[simp]

theorem nilradical_eq_zero (R : Type u_3) [CommSemiring R] [IsReduced R] :

nilradical R = 0

@[simp]

theorem LinearMap.isNilpotent_mulLeft_iff (R : Type u_1) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :

IsNilpotent (LinearMap.mulLeft R a) ↔ IsNilpotent a

@[simp]

theorem LinearMap.isNilpotent_mulRight_iff (R : Type u_1) {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (a : A) :

IsNilpotent (LinearMap.mulRight R a) ↔ IsNilpotent a

@[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) :

IsNilpotent ((LinearMap.toMatrix b b) f) ↔ IsNilpotent f

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 (Submodule.mapQ p p f hp)

theorem NoZeroSMulDivisors.isReduced (R : Type u_3) (M : Type u_4) [MonoidWithZero R] [Zero M] [MulActionWithZero R M] [Nontrivial M] [NoZeroSMulDivisors R M] :