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
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
simp_rw [isReduced_iff, hf.forall, IsNilpotent, ← map_pow, ← RingHom.mem_ker]
no goals
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
rfl