mathlib

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

feat(src/ring_theory): in a PID, all fractional ideals are invertible (#2826) This would show that all PIDs are Dedekind domains, once we have a definition of Dedekind domain (we could define it right now, but it would depend on the choice of field of fractions). In `localization.lean`, I added a few small lemmas on localizations (`localization.exists_integer_multiple` and `fraction_map.to_map_eq_zero_iff`). @101damnations, are these additions compatible with your branches? I'm happy to change them if not.