Commit 2020-08-17 21:27 f77530e9

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.