mathlib
fdbfe755 - chore(group_theory/group_action): Rename some group_action lemmas (#4946)

Commit
5 years ago
chore(group_theory/group_action): Rename some group_action lemmas (#4946) This renames * These lemmas about `group α`, for consistency with `smul_neg` etc, which are in the global scope: * `mul_action.inv_smul_smul` → `inv_smul_smul` * `mul_action.smul_inv_smul` → `smul_inv_smul` * `mul_action.inv_smul_eq_iff` → `inv_smul_eq_iff` * `mul_action.eq_inv_smul_iff` → `eq_inv_smul_iff` * These lemmas about `group_with_zero α`, for consistency with `smul_inv_smul'` etc, which have trailing `'`s (and were added in #2693, while the `'`-less ones were added later): * `inv_smul_eq_iff` → `inv_smul_eq_iff'` * `eq_inv_smul_iff` → `eq_inv_smul_iff'`
Author
Parents
Loading