Commit 2022-04-29 00:29 11a4a745

feat(ring_theory/localization/basic): generalize to semiring (#13459) The main ingredient of this PR is the definition of is_localization.lift that works for semirings. The previous definition uses ring_hom.mk' that essentially states that f 0 = 0 follows from other conditions. This does not holds for semirings. Instead, this PR defines the localization of monoid with zero, and uses this to define is_localization.lift.

• I think definitions around localization_with_zero_map might be ad hoc, and any suggestions for improvement are welcome!
• I plan to further generalize the localization API for semirings. This needs generalization of other ring theory stuff such as local_ring and is_domain (generalizing local_ring is partially done in #13341).