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 ⋯ ⋯