Commit 2022-05-06 18:45 8f116f43

feat(ring_theory/localization): generalize lemmas from comm_ring to comm_semiring (#13994) This PR does not add new stuffs, but removes several subtractions from the proofs.