Group actions on and by units M
#
This file provides the action of a unit on a type α
, has_scalar (units M) α
, in the presence of
has_scalar M α
, with the obvious definition stated in units.smul_def
. This definition preserves
mul_action
and distrib_mul_action
structures too.
Additionally, a mul_action G M
for some group G
satisfying some additional properties admits a
mul_action G (units M)
structure, again with the obvious definition stated in units.coe_smul
.
These instances use a primed name.
The results are repeated for add_units
and has_vadd
where relevant.
Action of the units of M
on a type α
#
Equations
Equations
- units.mul_action = {to_has_scalar := units.has_scalar mul_action.to_has_scalar, one_smul := _, mul_smul := _}
Equations
Equations
If an action G
associates and commutes with multiplication on M
, then it lifts to an
action on units M
. Notably, this provides mul_action (units M) (units N)
under suitable
conditions.
Note that this lemma exists more generally as the global smul_inv
Transfer smul_comm_class G H M
to smul_comm_class G H (units M)
Transfer is_scalar_tower G H M
to is_scalar_tower G H (units M)
Transfer is_scalar_tower G M α
to is_scalar_tower G (units M) α
A stronger form of units.mul_action'
.
Equations
- units.mul_distrib_mul_action' = {to_mul_action := {to_has_scalar := {smul := has_scalar.smul mul_action.to_has_scalar}, one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}