English
For a commutative semiring R and p ≥ 1, x ∈ pNilradical R p iff there exists n with x^{p^n}=0.
Русский
Для R коммутативного полус и p: x ∈ pNilradical R p эквивалентно существованию n с x^{p^n}=0.
LaTeX
$$$$ x \\in pNilradical(R,p) \\iff \\exists n:\\mathbb{N}, \\; x^{p^{n}}=0. $$$$
Lean4
theorem mem_pNilradical {R : Type*} [CommSemiring R] {p : ℕ} {x : R} : x ∈ pNilradical R p ↔ ∃ n : ℕ, x ^ p ^ n = 0 :=
by
by_cases hp : 1 < p
· rw [pNilradical_eq_nilradical hp]
refine ⟨fun ⟨n, h⟩ ↦ ⟨n, ?_⟩, fun ⟨n, h⟩ ↦ ⟨p ^ n, h⟩⟩
rw [← Nat.sub_add_cancel ((n.lt_pow_self hp).le), pow_add, h, mul_zero]
rw [pNilradical_eq_bot hp, Ideal.mem_bot]
refine ⟨fun h ↦ ⟨0, by rw [pow_zero, pow_one, h]⟩, fun ⟨n, h⟩ ↦ ?_⟩
rcases Nat.le_one_iff_eq_zero_or_eq_one.1 (not_lt.1 hp) with hp | hp
· by_cases hn : n = 0
· rwa [hn, pow_zero, pow_one] at h
rw [hp, zero_pow hn, pow_zero] at h
subsingleton [subsingleton_of_zero_eq_one h.symm]
rwa [hp, one_pow, pow_one] at h
