Commit 2025-10-28 12:15 1d861322
View on Github →feat(Localization): r / m in the localisation is regular iff r is (#30708)
Also rename IsLocalization.mk'_surjective to IsLocalization.exists_mk'_eq because it takes the name of the lemma I need.