Commit 2024-01-27 19:32 09b44c17

feat(GroupTheory/GroupAction/Group): invOf smul lemmas (#9972) Give smul versions of some existing mul lemmas:

• invOf_smul_smul
• smul_invOf_smul (c.f. mul_invOf_self_assoc)
• invOf_smul_eq_iff (c.f. invOf_mul_eq_iff_eq_mul_left) (required for #7569)
• smul_eq_iff_eq_invOf_smul (c.f mul_left_eq_iff_eq_invOf_mul)