Group actions on and by Mˣ #
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
MulAction and DistribMulAction structures too.
Additionally, a MulAction G M for some group G satisfying some additional properties admits a
MulAction G Mˣ structure, again with the obvious definition stated in Units.coe_smul.
These instances use a primed name.
The results are repeated for AddUnits and VAdd where relevant.
Action of the units of M on a type α #
instance
Units.instSMulZeroClass
{M : Type u_3}
{α : Type u_5}
[Monoid M]
[Zero α]
[SMulZeroClass M α]
:
SMulZeroClass Mˣ α
Equations
- Units.instSMulZeroClass = SMulZeroClass.mk ⋯
instance
Units.instDistribSMulUnits
{M : Type u_3}
{α : Type u_5}
[Monoid M]
[AddZeroClass α]
[DistribSMul M α]
:
DistribSMul Mˣ α
Equations
- Units.instDistribSMulUnits = DistribSMul.mk ⋯
instance
Units.instDistribMulAction
{M : Type u_3}
{α : Type u_5}
[Monoid M]
[AddMonoid α]
[DistribMulAction M α]
:
Equations
- Units.instDistribMulAction = let __spread.0 := Units.instDistribSMulUnits; DistribMulAction.mk ⋯ ⋯
instance
Units.instMulDistribMulAction
{M : Type u_3}
{α : Type u_5}
[Monoid M]
[Monoid α]
[MulDistribMulAction M α]
:
Equations
- Units.instMulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯
Action of a group G on units of M #
instance
Units.mulDistribMulAction'
{G : Type u_1}
{M : Type u_3}
[Group G]
[Monoid M]
[MulDistribMulAction G M]
[SMulCommClass G M M]
[IsScalarTower G M M]
:
A stronger form of Units.mul_action'.
Equations
- Units.mulDistribMulAction' = let __src := Units.mulAction'; MulDistribMulAction.mk ⋯ ⋯