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})
R S : Type u
x y : R
inst✝ : CommSemiring R
⊢ IsRadical y ↔ Ideal.IsRadical (Ideal.span {y})
simp_rw [IsRadical, ← Ideal.mem_span_singleton]
no goals
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})
exact forall_swap.trans (forall_congr' fun r => exists_imp.symm)