Equations
- Multiplicative.smul = { smul := fun (a : Multiplicative α) (x : β) => Multiplicative.toAdd a +ᵥ x }
@[simp]
Equations
- Additive.addAction = AddAction.mk ⋯ ⋯
instance
Multiplicative.mulAction
{α : Type u_5}
{β : Type u_6}
[AddMonoid α]
[AddAction α β]
:
MulAction (Multiplicative α) β
Equations
- Multiplicative.mulAction = MulAction.mk ⋯ ⋯
instance
Additive.vaddCommClass
{α : Type u_5}
{β : Type u_6}
{γ : Type u_7}
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
VAddCommClass (Additive α) (Additive β) γ
Equations
- ⋯ = ⋯
instance
Multiplicative.smulCommClass
{α : Type u_5}
{β : Type u_6}
{γ : Type u_7}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
SMulCommClass (Multiplicative α) (Multiplicative β) γ
Equations
- ⋯ = ⋯
def
AddAction.toEndHom
{M : Type u_1}
{α : Type u_5}
[AddMonoid M]
[AddAction M α]
:
M →+ Additive (Function.End α)
The additive monoid hom representing an additive monoid action.
When M
is a group, see AddAction.toPermHom
.
Equations
- AddAction.toEndHom = MonoidHom.toAdditive'' MulAction.toEndHom
Instances For
@[reducible, inline]
abbrev
AddAction.ofEndHom
{M : Type u_1}
{α : Type u_5}
[AddMonoid M]
(f : M →+ Additive (Function.End α))
:
AddAction M α
The additive action induced by a hom to Additive (Function.End α)
See note [reducible non-instances].