# 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

- Additive.addAction = { toVAdd := Additive.vadd, zero_vadd := ⋯, add_vadd := ⋯ }

source
instance Multiplicative.mulAction {α : Type u_2} {β : Type u_3} [AddMonoid α] [AddAction α β] :
MulAction (Multiplicative α) β
Equations

- Multiplicative.mulAction = { toSMul := Multiplicative.smul, one_smul := ⋯, mul_smul := ⋯ }

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 β) γ