mathlib3
8f116f43 - feat(ring_theory/localization): generalize lemmas from `comm_ring` to `comm_semiring` (#13994)

Commit

3 years ago

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.

Author

yuma-mizuno

Parents

27e105d2

mathlib3 8f116f43 - feat(ring_theory/localization): generalize lemmas from `comm_ring` to `comm_semiring` (#13994)

mathlib3
8f116f43 - feat(ring_theory/localization): generalize lemmas from `comm_ring` to `comm_semiring` (#13994)