mathlib3

694da7e2 - feat(ring_theory): the surjective image of a PID is a PID (#9069)

feat(ring_theory): the surjective image of a PID is a PID (#9069) If the preimage of an ideal/submodule under a surjective map is principal, so is the original ideal. Therefore, the image of a principal ideal domain under a surjective ring hom is again a PID.