Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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`) Co-authored-by: Christopher Hoskin <[email protected]> Co-authored-by: Christopher Hoskin <[email protected]>
- Loading branch information