Additive and Multiplicative for group actions

Tags

group action

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

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

Home · Documentation · Publications · Contributors · Source · Cite