Documentation

Mathlib.Algebra.Group.Action.TypeTags

Additive and Multiplicative for group actions #

Tags #

group action

instance Additive.vadd {α : Type u_5} {β : Type u_6} [SMul α β] :
VAdd (Additive α) β
Equations
  • Additive.vadd = { vadd := fun (a : Additive α) (x : β) => Additive.toMul a x }
instance Multiplicative.smul {α : Type u_5} {β : Type u_6} [VAdd α β] :
Equations
  • Multiplicative.smul = { smul := fun (a : Multiplicative α) (x : β) => Multiplicative.toAdd a +ᵥ x }
@[simp]
theorem toMul_smul {α : Type u_5} {β : Type u_6} [SMul α β] (a : Additive α) (b : β) :
Additive.toMul a b = a +ᵥ b
@[simp]
theorem ofMul_vadd {α : Type u_5} {β : Type u_6} [SMul α β] (a : α) (b : β) :
Additive.ofMul a +ᵥ b = a b
@[simp]
theorem toAdd_vadd {α : Type u_5} {β : Type u_6} [VAdd α β] (a : Multiplicative α) (b : β) :
Multiplicative.toAdd a +ᵥ b = a b
@[simp]
theorem ofAdd_smul {α : Type u_5} {β : Type u_6} [VAdd α β] (a : α) (b : β) :
Multiplicative.ofAdd a b = a +ᵥ b
instance Additive.addAction {α : Type u_5} {β : Type u_6} [Monoid α] [MulAction α β] :
Equations
instance Multiplicative.mulAction {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddAction α β] :
Equations
instance Additive.vaddCommClass {α : Type u_5} {β : Type u_6} {γ : Type u_7} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
Equations
  • =
instance Multiplicative.smulCommClass {α : Type u_5} {β : Type u_6} {γ : Type u_7} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
Equations
  • =

The tautological additive action by Additive (Function.End α) on α.

Equations
  • AddAction.functionEnd = inferInstance
def AddAction.toEndHom {M : Type u_1} {α : Type u_5} [AddMonoid M] [AddAction M α] :

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 α)) :

    The additive action induced by a hom to Additive (Function.End α)

    See note [reducible non-instances].

    Equations
    Instances For