Theorem isLeftRegular_iff_isRegular

Modification history

2025-11-21 13:53
Mathlib/Algebra/Group/Defs.lean
chore(Algebra/Group/Defs): missing `to_additive` (#31890)
Modified isLeftRegular_iff_isRegularView on Github →
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 →