R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ IsRadical (RingHom.ker (Quotient.mk I)) ↔ IsReduced (R ⧸ I)
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ IsRadical I ↔ IsReduced (R ⧸ I)
conv_lhs => rw [← @Ideal.mk_ker R _ I]
no goals
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ IsRadical (RingHom.ker (Quotient.mk I)) ↔ IsReduced (R ⧸ I)
exact RingHom.ker_isRadical_iff_reduced_of_surjective (@Ideal.Quotient.mk_surjective R _ I)