Theorem isSMulRegular_of_group

Modification history

2026-09-09 05:30
Mathlib/Algebra/Regular/SMul.lean
feat(Algebra/Regular/SMul): add IsSMulRegular.all (#43600) …
Modified isSMulRegular_of_groupView on Github →
2022-12-22 01:22
Mathlib/Algebra/Regular/SMul.lean
Feat: port algebra.regular.smul (#1154) …
Added isSMulRegular_of_groupView on Github →