Theorem smul_eq_iff_eq_invOf_smul

Modification history

2024-07-16 22:43

Mathlib/Algebra/Group/Action/Basic.lean

chore: Move group lemmas out of `GroupTheory.GroupAction.Group` (#14705) …

Modified smul_eq_iff_eq_invOf_smul View on Github →

2024-01-27 19:32

Mathlib/GroupTheory/GroupAction/Group.lean

feat(GroupTheory/GroupAction/Group): invOf smul lemmas (#9972) …

Added smul_eq_iff_eq_invOf_smul View on Github →