theorem Ideal.map_nilradical_le {R : Type u_1} {S : Type u_2} {F : Type u_3} [CommSemiring R] [CommSemiring S] [FunLike F R S] [RingHomClass F R S] (f : F) : map f (nilradical R) ≤ nilradical S