Theorem isLeftRegular_iff_isRegular

Modification history

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