mathlib3

f77530e9 - feat(ring_theory/localization): Generalize theorems about localization over an integral domain (#3780)

feat(ring_theory/localization): Generalize theorems about localization over an integral domain (#3780) A number of theorems about the `fraction_map` from an integral domain to its field of fractions can be generalized to apply to any `localization_map` that were the localization set doesn't contain any zero divisors. The main use for this is to show that localizing an integral domain at any set of non-zero elements is an integral domain, were previously this was only proven for the field of fractions. I made `le_non_zero_divisors` a class so that the integral domain instance can be synthesized automatically once you show that zero isn't in the localization set, but it could be left as just a proposition instead if that seems unnecessary.