English
The perfect closure is a reduced ring: it has no nonzero nilpotent elements.
Русский
Совершённое замыкание является редуцированным кольцом: не существует ненулевых нильпотентных элементов.
LaTeX
$$$\operatorname{IsReduced}\bigl(\mathrm{PerfectClosure}(K,p)\bigr).$$$
Lean4
instance instReduced : IsReduced (PerfectClosure K p) where
eq_zero
x :=
induction_on x fun x ⟨n, h⟩ ↦
by
replace h : mk K p x ^ p ^ n = 0 := by
rw [← Nat.sub_add_cancel ((n.lt_pow_self (Fact.out : p.Prime).one_lt).le), pow_add, h, mul_zero]
simp only [zero_def, mk_pow, mk_eq_iff, zero_add, ← coe_iterateFrobenius, map_zero] at h ⊢
obtain ⟨m, h⟩ := h
exact ⟨n + m, by simpa only [iterateFrobenius_def, pow_add, pow_mul] using h⟩
