Multiplicative actions with zero on and by Mˣ #
This file provides the multiplicative actions with zero of a unit on a type α, SMul Mˣ α, in the
presence of SMulWithZero M α, with the obvious definition stated in Units.smul_def.
Additionally, a MulDistribMulAction G M for some group G satisfying some additional properties
admits a MulDistribMulAction G Mˣ structure, again with the obvious definition stated in
Units.coe_smul. This instance uses a primed name.
See also #
Algebra.GroupWithZero.Action.OppositeAlgebra.GroupWithZero.Action.PiAlgebra.GroupWithZero.Action.Prod
Action of the units of M on a type α #
instance
Units.instSMulZeroClass
{M : Type u_2}
{α : Type u_3}
[Monoid M]
[Zero α]
[SMulZeroClass M α]
:
SMulZeroClass Mˣ α
Equations
- Units.instSMulZeroClass = SMulZeroClass.mk ⋯
instance
Units.instDistribSMulUnits
{M : Type u_2}
{α : Type u_3}
[Monoid M]
[AddZeroClass α]
[DistribSMul M α]
:
DistribSMul Mˣ α
Equations
- Units.instDistribSMulUnits = DistribSMul.mk ⋯
instance
Units.instDistribMulAction
{M : Type u_2}
{α : Type u_3}
[Monoid M]
[AddMonoid α]
[DistribMulAction M α]
:
Equations
- Units.instDistribMulAction = let __spread.0 := Units.instDistribSMulUnits; DistribMulAction.mk ⋯ ⋯
instance
Units.instMulDistribMulAction
{M : Type u_2}
{α : Type u_3}
[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_2}
[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 ⋯ ⋯