Theorem localization.exists_integer_multiple'

feat(ring/localization): add construction of localization as a quotient type (#2922)

feat(src/ring_theory): in a PID, all fractional ideals are invertible (#2826) …