Theorem IsLocalization.isRegular_mk'

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.isRegular_mk'View on Github →