Additive and Multiplicative for group actions

Tags

group action

instance Additive.vadd {α : Type u_2} {β : Type u_3} [SMul α β] : VAdd (Additive α) β

Equations

• Additive.vadd = { vadd := fun (a : Additive α) (x : β) => Additive.toMul a • x }

instance Multiplicative.smul {α : Type u_2} {β : Type u_3} [VAdd α β] : SMul (Multiplicative α) β

Equations

• Multiplicative.smul = { smul := fun (a : Multiplicative α) (x : β) => Multiplicative.toAdd a +ᵥ x }

@[simp]

theorem toMul_smul {α : Type u_2} {β : Type u_3} [SMul α β] (a : Additive α) (b : β) : Additive.toMul a • b = a +ᵥ b

@[simp]

theorem ofMul_vadd {α : Type u_2} {β : Type u_3} [SMul α β] (a : α) (b : β) : Additive.ofMul a +ᵥ b = a • b

@[simp]

theorem toAdd_vadd {α : Type u_2} {β : Type u_3} [VAdd α β] (a : Multiplicative α) (b : β) : Multiplicative.toAdd a +ᵥ b = a • b

@[simp]

theorem ofAdd_smul {α : Type u_2} {β : Type u_3} [VAdd α β] (a : α) (b : β) : Multiplicative.ofAdd a • b = a +ᵥ b

instance Additive.addAction {α : Type u_2} {β : Type u_3} [Monoid α] [MulAction α β] : AddAction (Additive α) β

Equations

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

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

Equations

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

instance Additive.vaddCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] : VAddCommClass (Additive α) (Additive β) γ

instance Multiplicative.smulCommClass {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] : SMulCommClass (Multiplicative α) (Multiplicative β) γ