R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
hK : IsRadical K
⊢ IsRadical (Ideal.radical (Ideal.comap f K))
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
hK : IsRadical K
⊢ IsRadical (Ideal.comap f K)
rw [← hK.radical, comap_radical]
no goals
R : Type u
S : Type v
F : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
rc : RingHomClass F R S
f : F
I J : Ideal R
K L : Ideal S
hK : IsRadical K
⊢ IsRadical (Ideal.radical (Ideal.comap f K))
apply radical_isRadical