Commit 2024-09-29 14:29 cda107d6
View on Github →feat(RingTheory/Localization): some API on localizations (#17030) This PR adds some API for localizations of rings. In particular:
- localizations commute with localizations
- localizing away from a product of elements is the same as successive localization at the elements