mathlib3

11a4a745 - feat(ring_theory/localization/basic): generalize to semiring (#13459)

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).