# Commit 2021-05-25 11:18 4abbe10d

View on Github →feat(group_theory/group_action/units): group actions on and by units (#7438)
This removes all the lemmas about `(u : α) • x`

and `(↑u⁻¹ : α) • x`

in favor of granting `units α`

its very own `has_scalar`

structure, along with providing the stronger variants to make it usable elsewhere.
This means that downstream code need only reason about `[group G] [mul_action G M]`

instead of needing to handle groups and `units`

separately.
The (multiplicative versions of the) removed and moved lemmas are:

`units.inv_smul_smul`

→`inv_smul_smul`

`units.smul_inv_smul`

→`smul_inv_smul`

`units.smul_perm_hom`

,`mul_action.to_perm`

→`mul_action.to_perm_hom`

`units.smul_perm`

→`mul_action.to_perm`

`units.smul_left_cancel`

→`smul_left_cancel`

`units.smul_eq_iff_eq_inv_smul`

→`smul_eq_iff_eq_inv_smul`

`units.smul_eq_zero`

→`smul_eq_zero_iff_eq`

(to avoid clashing with`smul_eq_zero`

)`units.smul_ne_zero`

→`smul_ne_zero_iff_ne`

`homeomorph.smul_of_unit`

→`homeomorph.smul`

(the latter already existed, and the former was a special case)`units.measurable_const_smul_iff`

→`measurable_const_smul_iff`

`units.ae_measurable_const_smul_iff`

→`ae_measurable_const_smul_iff`

The new lemmas are:`smul_eq_zero_iff_eq'`

, a`group_with_zero`

version of`smul_eq_zero_iff_eq`

`smul_ne_zero_iff_ne'`

, a`group_with_zero`

version of`smul_ne_zero_iff_ne`

`units.neg_smul`

, a version of`neg_smul`

for units. We don't currently have typeclasses about`neg`

on objects without`+`

. We also end up needing some new typeclass instances downstream`units.measurable_space`

`units.has_measurable_smul`

`units.has_continuous_smul`

This goes on to remove lots of coercions from`alternating_map`

,`matrix.det`

, and some lie algebra stuff. This makes the theorem statement cleaner, but occasionally requires rewriting through`units.smul_def`

to add or remove the coercion.