Theorem IsLocalization.exists_mk'_eq

Modification history

2025-10-28 12:15
Mathlib/RingTheory/Localization/Defs.lean
feat(Localization): `r / m` in the localisation is regular iff `r` is (#30708) …
Added IsLocalization.exists_mk'_eqView on Github →