Commit 2026-02-04 10:57 6f67232d
View on Github →refactor(GroupTheory/MonoidLocalization): split long file (#34811)
Shorten the long file MonoidLocalization.Basic by splitting off a chunk of theory about mapping properties of localization (extending maps out of M to localizations of M under suitable conditions) into a new file MonoidLocalization.Maps. This shortens the Basic file from 1500 lines to 900.