Documentation

Mathlib.Algebra.Group.Action.TypeTags

Additive and Multiplicative for group actions #

Tags #

group action

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

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

Equations
  • AddAction.functionEnd = inferInstance
source
def AddAction.toEndHom {M : Type u_1} {α : Type u_2} [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
    source
    @[reducible, inline]
    abbrev AddAction.ofEndHom {M : Type u_1} {α : Type u_2} [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].

    Equations
    Instances For