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

Estimated changes