Group actions on and by
This file provides the action of a unit on a type
SMul Mˣ α, in the presence of
SMul M α, with the obvious definition stated in
Units.smul_def. This definition preserves
DistribMulAction structures too.
MulAction G M for some group
G satisfying some additional properties admits a
MulAction G Mˣ structure, again with the obvious definition stated in
These instances use a primed name.
The results are repeated for
VAdd where relevant.
Action of the units of
M on a type
- (_ : FaithfulVAdd (AddUnits M) α) = (_ : FaithfulVAdd (AddUnits M) α)
- Units.instSMulZeroClassUnits = SMulZeroClass.mk (_ : ∀ (m : Mˣ), ↑m • 0 = 0)
- One or more equations did not get rendered due to their size.
Action of a group
G on units of
If an action
G associates and commutes with multiplication on
M, then it lifts to an
Mˣ. Notably, this provides
mul_action Mˣ Nˣ under suitable
SMulCommClass G H M to
SMulCommClass G H Mˣ
IsScalarTower G H M to
IsScalarTower G H Mˣ
IsScalarTower G M α to
IsScalarTower G Mˣ α
A stronger form of