[GOAL]
R S : Type u
x y : R
inst✝ : Ring R
h : IsNilpotent x
⊢ IsNilpotent (-x)
[PROOFSTEP]
obtain ⟨n, hn⟩ := h
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Ring R
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (-x)
[PROOFSTEP]
use n
[GOAL]
case h
R S : Type u
x y : R
inst✝ : Ring R
n : ℕ
hn : x ^ n = 0
⊢ (-x) ^ n = 0
[PROOFSTEP]
rw [neg_pow, hn, mul_zero]
[GOAL]
R S : Type u
x y : R
inst✝² : MonoidWithZero R
inst✝¹ : MonoidWithZero S
r : R
F : Type u_1
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ IsNilpotent (↑f r)
[PROOFSTEP]
use hr.choose
[GOAL]
case h
R S : Type u
x y : R
inst✝² : MonoidWithZero R
inst✝¹ : MonoidWithZero S
r : R
F : Type u_1
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ ↑f r ^ Exists.choose hr = 0
[PROOFSTEP]
rw [← map_pow, hr.choose_spec, map_zero]
[GOAL]
R S : Type u
x y : R
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r - 1)
[PROOFSTEP]
obtain ⟨n, hn⟩ := hnil
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ IsUnit (r - 1)
[PROOFSTEP]
refine' ⟨⟨r - 1, -∑ i in Finset.range n, r ^ i, _, _⟩, rfl⟩
[GOAL]
case intro.refine'_1
R S : Type u
x y : R
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (r - 1) * -∑ i in Finset.range n, r ^ i = 1
[PROOFSTEP]
rw [mul_neg, mul_geom_sum, hn]
[GOAL]
case intro.refine'_1
R S : Type u
x y : R
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ -(0 - 1) = 1
[PROOFSTEP]
simp
[GOAL]
case intro.refine'_2
R S : Type u
x y : R
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ (-∑ i in Finset.range n, r ^ i) * (r - 1) = 1
[PROOFSTEP]
rw [neg_mul, geom_sum_mul, hn]
[GOAL]
case intro.refine'_2
R S : Type u
x y : R
inst✝ : Ring R
r : R
n : ℕ
hn : r ^ n = 0
⊢ -(0 - 1) = 1
[PROOFSTEP]
simp
[GOAL]
R S : Type u
x y : R
inst✝ : Ring R
r : R
u : Rˣ
hnil : IsNilpotent r
hru : Commute r ↑u⁻¹
⊢ IsUnit (↑u + r)
[PROOFSTEP]
rw [← Units.isUnit_mul_units _ u⁻¹, add_mul, Units.mul_inv, ← IsUnit.neg_iff, add_comm, neg_add, ← sub_eq_add_neg]
[GOAL]
R S : Type u
x y : R
inst✝ : Ring R
r : R
u : Rˣ
hnil : IsNilpotent r
hru : Commute r ↑u⁻¹
⊢ IsUnit (-(r * ↑u⁻¹) - 1)
[PROOFSTEP]
obtain ⟨n, hn⟩ := hnil
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Ring R
r : R
u : Rˣ
hru : Commute r ↑u⁻¹
n : ℕ
hn : r ^ n = 0
⊢ IsUnit (-(r * ↑u⁻¹) - 1)
[PROOFSTEP]
refine' IsNilpotent.sub_one_isUnit ⟨n, _⟩
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Ring R
r : R
u : Rˣ
hru : Commute r ↑u⁻¹
n : ℕ
hn : r ^ n = 0
⊢ (-(r * ↑u⁻¹)) ^ n = 0
[PROOFSTEP]
rw [neg_pow, hru.mul_pow, hn]
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Ring R
r : R
u : Rˣ
hru : Commute r ↑u⁻¹
n : ℕ
hn : r ^ n = 0
⊢ (-1) ^ n * (0 * ↑u⁻¹ ^ n) = 0
[PROOFSTEP]
simp
[GOAL]
R S : Type u
x y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
⊢ IsReduced R
[PROOFSTEP]
constructor
[GOAL]
case eq_zero
R S : Type u
x y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
⊢ ∀ (x : R), IsNilpotent x → x = 0
[PROOFSTEP]
intro x hx
[GOAL]
case eq_zero
R S : Type u
x✝ y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ x = 0
[PROOFSTEP]
apply hf
[GOAL]
case eq_zero.a
R S : Type u
x✝ y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ ↑f x = ↑f 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
case eq_zero.a
R S : Type u
x✝ y : R
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
F : Type u_1
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ↑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ ↑f x = 0
[PROOFSTEP]
exact (hx.map f).eq_zero
[GOAL]
R S✝ : Type u
x y : R
S : Type u_1
F : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
⊢ Ideal.IsRadical (ker f) ↔ IsReduced S
[PROOFSTEP]
simp_rw [isReduced_iff, hf.forall, IsNilpotent, ← map_pow, ← RingHom.mem_ker]
[GOAL]
R S✝ : Type u
x y : R
S : Type u_1
F : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommRing S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ↑f
⊢ Ideal.IsRadical (ker f) ↔ ∀ (x : R), (∃ n, x ^ n ∈ ker f) → x ∈ ker f
[PROOFSTEP]
rfl
[GOAL]
R S : Type u
x y : R
inst✝ : MonoidWithZero R
⊢ IsRadical 0 ↔ IsReduced R
[PROOFSTEP]
simp_rw [isReduced_iff, IsNilpotent, exists_imp, ← zero_dvd_iff]
[GOAL]
R S : Type u
x y : R
inst✝ : MonoidWithZero R
⊢ IsRadical 0 ↔ ∀ (x : R) (x_1 : ℕ), 0 ∣ x ^ x_1 → 0 ∣ x
[PROOFSTEP]
exact forall_swap
[GOAL]
R S : Type u
x y : R
inst✝ : CommSemiring R
⊢ IsRadical y ↔ Ideal.IsRadical (Ideal.span {y})
[PROOFSTEP]
simp_rw [IsRadical, ← Ideal.mem_span_singleton]
[GOAL]
R S : Type u
x y : R
inst✝ : CommSemiring R
⊢ (∀ (n : ℕ) (x : R), x ^ n ∈ Ideal.span {y} → x ∈ Ideal.span {y}) ↔ Ideal.IsRadical (Ideal.span {y})
[PROOFSTEP]
exact forall_swap.trans (forall_congr' fun r => exists_imp.symm)
[GOAL]
R S : Type u
x y : R
inst✝ : MonoidWithZero R
k : ℕ
hk : 1 < k
⊢ IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0
[PROOFSTEP]
simp_rw [← zero_isRadical_iff, isRadical_iff_pow_one_lt k hk, zero_dvd_iff]
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x + y)
[PROOFSTEP]
obtain ⟨n, hn⟩ := hx
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : IsNilpotent y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x + y)
[PROOFSTEP]
obtain ⟨m, hm⟩ := hy
[GOAL]
case intro.intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ IsNilpotent (x + y)
[PROOFSTEP]
use n + m - 1
[GOAL]
case h
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ (x + y) ^ (n + m - 1) = 0
[PROOFSTEP]
rw [h_comm.add_pow']
[GOAL]
case h
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ ∑ m_1 in Finset.Nat.antidiagonal (n + m - 1), Nat.choose (n + m - 1) m_1.fst • (x ^ m_1.fst * y ^ m_1.snd) = 0
[PROOFSTEP]
apply Finset.sum_eq_zero
[GOAL]
case h.h
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
⊢ ∀ (x_1 : ℕ × ℕ),
    x_1 ∈ Finset.Nat.antidiagonal (n + m - 1) → Nat.choose (n + m - 1) x_1.fst • (x ^ x_1.fst * y ^ x_1.snd) = 0
[PROOFSTEP]
rintro ⟨i, j⟩ hij
[GOAL]
case h.h.mk
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
⊢ Nat.choose (n + m - 1) (i, j).fst • (x ^ (i, j).fst * y ^ (i, j).snd) = 0
[PROOFSTEP]
suffices x ^ i * y ^ j = 0 by simp only [this, nsmul_eq_mul, mul_zero]
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
this : x ^ i * y ^ j = 0
⊢ Nat.choose (n + m - 1) (i, j).fst • (x ^ (i, j).fst * y ^ (i, j).snd) = 0
[PROOFSTEP]
simp only [this, nsmul_eq_mul, mul_zero]
[GOAL]
case h.h.mk
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
⊢ x ^ i * y ^ j = 0
[PROOFSTEP]
cases' Nat.le_or_le_of_add_eq_add_pred (Finset.Nat.mem_antidiagonal.mp hij) with hi hj
[GOAL]
case h.h.mk.inl
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
hi : n ≤ (i, j).fst
⊢ x ^ i * y ^ j = 0
[PROOFSTEP]
rw [pow_eq_zero_of_le hi hn, zero_mul]
[GOAL]
case h.h.mk.inr
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
m : ℕ
hm : y ^ m = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal (n + m - 1)
hj : m ≤ (i, j).snd
⊢ x ^ i * y ^ j = 0
[PROOFSTEP]
rw [pow_eq_zero_of_le hj hm, mul_zero]
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝ : Commute x y
ι : Type u_1
s : Finset ι
f : ι → R
hnp : ∀ (i : ι), i ∈ s → IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)
⊢ IsNilpotent (∑ i in s, f i)
[PROOFSTEP]
classical
induction' s using Finset.induction with j s hj ih; simp
rw [Finset.sum_insert hj]
apply Commute.isNilpotent_add
· exact Commute.sum_right _ _ _ (fun i hi ↦ h_comm _ _ (by simp) (by simp [hi]))
· apply hnp; simp
· exact ih (fun i hi ↦ hnp i (by simp [hi])) (fun i j hi hj ↦ h_comm i j (by simp [hi]) (by simp [hj]))
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝ : Commute x y
ι : Type u_1
s : Finset ι
f : ι → R
hnp : ∀ (i : ι), i ∈ s → IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)
⊢ IsNilpotent (∑ i in s, f i)
[PROOFSTEP]
induction' s using Finset.induction with j s hj ih
[GOAL]
case empty
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)
hnp : ∀ (i : ι), i ∈ ∅ → IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ ∅ → j ∈ ∅ → Commute (f i) (f j)
⊢ IsNilpotent (∑ i in ∅, f i)
case insert
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (∑ i in insert j s, f i)
[PROOFSTEP]
simp
[GOAL]
case insert
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (∑ i in insert j s, f i)
[PROOFSTEP]
rw [Finset.sum_insert hj]
[GOAL]
case insert
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (f j + ∑ x in s, f x)
[PROOFSTEP]
apply Commute.isNilpotent_add
[GOAL]
case insert.h_comm
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ Commute (f j) (∑ x in s, f x)
[PROOFSTEP]
exact Commute.sum_right _ _ _ (fun i hi ↦ h_comm _ _ (by simp) (by simp [hi]))
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
i : ι
hi : i ∈ s
⊢ j ∈ insert j s
[PROOFSTEP]
simp
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
i : ι
hi : i ∈ s
⊢ i ∈ insert j s
[PROOFSTEP]
simp [hi]
[GOAL]
case insert.hx
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (f j)
[PROOFSTEP]
apply hnp
[GOAL]
case insert.hx.a
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ j ∈ insert j s
[PROOFSTEP]
simp
[GOAL]
case insert.hy
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
⊢ IsNilpotent (∑ x in s, f x)
[PROOFSTEP]
exact ih (fun i hi ↦ hnp i (by simp [hi])) (fun i j hi hj ↦ h_comm i j (by simp [hi]) (by simp [hj]))
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j : ι
s : Finset ι
hj : ¬j ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j s → IsNilpotent (f i)
h_comm : ∀ (i j_1 : ι), i ∈ insert j s → j_1 ∈ insert j s → Commute (f i) (f j_1)
i : ι
hi : i ∈ s
⊢ i ∈ insert j s
[PROOFSTEP]
simp [hi]
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j✝ : ι
s : Finset ι
hj✝ : ¬j✝ ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j✝ s → IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ insert j✝ s → j ∈ insert j✝ s → Commute (f i) (f j)
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ i ∈ insert j✝ s
[PROOFSTEP]
simp [hi]
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm✝¹ : Commute x y
ι : Type u_1
s✝ : Finset ι
f : ι → R
hnp✝ : ∀ (i : ι), i ∈ s✝ → IsNilpotent (f i)
h_comm✝ : ∀ (i j : ι), i ∈ s✝ → j ∈ s✝ → Commute (f i) (f j)
j✝ : ι
s : Finset ι
hj✝ : ¬j✝ ∈ s
ih :
  (∀ (i : ι), i ∈ s → IsNilpotent (f i)) →
    (∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)) → IsNilpotent (∑ i in s, f i)
hnp : ∀ (i : ι), i ∈ insert j✝ s → IsNilpotent (f i)
h_comm : ∀ (i j : ι), i ∈ insert j✝ s → j ∈ insert j✝ s → Commute (f i) (f j)
i j : ι
hi : i ∈ s
hj : j ∈ s
⊢ j ∈ insert j✝ s
[PROOFSTEP]
simp [hj]
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent x
⊢ IsNilpotent (x * y)
[PROOFSTEP]
obtain ⟨n, hn⟩ := h
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent (x * y)
[PROOFSTEP]
use n
[GOAL]
case h
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
n : ℕ
hn : x ^ n = 0
⊢ (x * y) ^ n = 0
[PROOFSTEP]
rw [h_comm.mul_pow, hn, zero_mul]
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
⊢ IsNilpotent (x * y) ↔ IsNilpotent x
[PROOFSTEP]
refine' ⟨_, h_comm.isNilpotent_mul_left⟩
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
⊢ IsNilpotent (x * y) → IsNilpotent x
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent x
[PROOFSTEP]
rw [mul_pow h_comm] at hk
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hy : y ∈ nonZeroDivisorsLeft R
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent x
[PROOFSTEP]
exact ⟨k, (nonZeroDivisorsLeft R).pow_mem hy k _ hk⟩
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (x * y)
[PROOFSTEP]
rw [h_comm.eq]
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (y * x)
[PROOFSTEP]
exact h_comm.symm.isNilpotent_mul_left h
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
⊢ IsNilpotent (x * y) ↔ IsNilpotent y
[PROOFSTEP]
refine' ⟨_, h_comm.isNilpotent_mul_right⟩
[GOAL]
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
⊢ IsNilpotent (x * y) → IsNilpotent y
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
k : ℕ
hk : (x * y) ^ k = 0
⊢ IsNilpotent y
[PROOFSTEP]
rw [mul_pow h_comm] at hk
[GOAL]
case intro
R S : Type u
x y : R
inst✝ : Semiring R
h_comm : Commute x y
hx : x ∈ nonZeroDivisorsRight R
k : ℕ
hk : x ^ k * y ^ k = 0
⊢ IsNilpotent y
[PROOFSTEP]
exact ⟨k, (nonZeroDivisorsRight R).pow_mem hx k _ hk⟩
[GOAL]
R S : Type u
x y : R
inst✝ : Ring R
h_comm : Commute x y
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)
[PROOFSTEP]
rw [← neg_right_iff] at h_comm
[GOAL]
R S : Type u
x y : R
inst✝ : Ring R
h_comm✝ : Commute x y
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent y
⊢ IsNilpotent (x - y)
[PROOFSTEP]
rw [← isNilpotent_neg_iff] at hy
[GOAL]
R S : Type u
x y : R
inst✝ : Ring R
h_comm✝ : Commute x y
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x - y)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
R S : Type u
x y : R
inst✝ : Ring R
h_comm✝ : Commute x y
h_comm : Commute x (-y)
hx : IsNilpotent x
hy : IsNilpotent (-y)
⊢ IsNilpotent (x + -y)
[PROOFSTEP]
exact h_comm.isNilpotent_add hx hy
[GOAL]
R✝ S : Type u
x✝ y✝ : R✝
inst✝¹ : CommSemiring R✝
x y : R✝
R : Type u_1
inst✝ : CommSemiring R
⊢ sInf {J | ⊥ ≤ J ∧ Ideal.IsPrime J} = sInf {J | Ideal.IsPrime J}
[PROOFSTEP]
simp_rw [and_iff_right bot_le]
[GOAL]
R S : Type u
x✝ y✝ : R
inst✝ : CommSemiring R
x y : R
⊢ IsNilpotent x ↔ ∀ (J : Ideal R), Ideal.IsPrime J → x ∈ J
[PROOFSTEP]
rw [← mem_nilradical, nilradical_eq_sInf, Submodule.mem_sInf]
[GOAL]
R S : Type u
x✝ y✝ : R
inst✝ : CommSemiring R
x y : R
⊢ (∀ (p : Submodule R R), p ∈ {J | Ideal.IsPrime J} → x ∈ p) ↔ ∀ (J : Ideal R), Ideal.IsPrime J → x ∈ J
[PROOFSTEP]
rfl
[GOAL]
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) ↔ IsNilpotent a
[PROOFSTEP]
constructor
[GOAL]
case mp
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulLeft R a) → IsNilpotent a
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case mpr
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulLeft R a)
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case mp.intro
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ IsNilpotent a
[PROOFSTEP]
use n
[GOAL]
case mpr.intro
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulLeft R a)
[PROOFSTEP]
use n
[GOAL]
case h
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulLeft R a ^ n = 0
⊢ a ^ n = 0
[PROOFSTEP]
simp only [mulLeft_eq_zero_iff, pow_mulLeft] at hn ⊢
[GOAL]
case h
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ mulLeft R a ^ n = 0
[PROOFSTEP]
simp only [mulLeft_eq_zero_iff, pow_mulLeft] at hn ⊢
[GOAL]
case h
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0
[PROOFSTEP]
exact hn
[GOAL]
case h
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0
[PROOFSTEP]
exact hn
[GOAL]
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) ↔ IsNilpotent a
[PROOFSTEP]
constructor
[GOAL]
case mp
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent (mulRight R a) → IsNilpotent a
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case mpr
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ IsNilpotent a → IsNilpotent (mulRight R a)
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case mp.intro
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ IsNilpotent a
[PROOFSTEP]
use n
[GOAL]
case mpr.intro
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ IsNilpotent (mulRight R a)
[PROOFSTEP]
use n
[GOAL]
case h
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : mulRight R a ^ n = 0
⊢ a ^ n = 0
[PROOFSTEP]
simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢
[GOAL]
case h
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ mulRight R a ^ n = 0
[PROOFSTEP]
simp only [mulRight_eq_zero_iff, pow_mulRight] at hn ⊢
[GOAL]
case h
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0
[PROOFSTEP]
exact hn
[GOAL]
case h
R S : Type u
x y : R
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
hn : a ^ n = 0
⊢ a ^ n = 0
[PROOFSTEP]
exact hn
[GOAL]
R S : Type u
x y : R
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
hnp : IsNilpotent f
⊢ IsNilpotent (Submodule.mapQ p p f hp)
[PROOFSTEP]
obtain ⟨k, hk⟩ := hnp
[GOAL]
case intro
R S : Type u
x y : R
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ IsNilpotent (Submodule.mapQ p p f hp)
[PROOFSTEP]
use k
[GOAL]
case h
R S : Type u
x y : R
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
k : ℕ
hk : f ^ k = 0
⊢ Submodule.mapQ p p f hp ^ k = 0
[PROOFSTEP]
simp [← p.mapQ_pow, hk]