feat(ring_theory/ideal_operations): correspondence under surjection (#534)
feat(ring_theory/ideal_operations): correspondence under surjection (#534)


leanprover-community/mathlib,leanprover-community/mathlib