Sum instances for additive and multiplicative actions

This file defines instances for additive and multiplicative actions on the binary Sum type.

See also

• Mathlib/Algebra/Group/Action/Option.lean
• Mathlib/Algebra/Group/Action/Pi.lean
• Mathlib/Algebra/Group/Action/Prod.lean
• Mathlib/Algebra/Group/Action/Sigma.lean

@[instance_reducible]

instance Sum.instSMul {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] : SMul M (α ⊕ β)

Equations

• Sum.instSMul = { smul := fun (a : M) => Sum.map (fun (x : α) => a • x) fun (x : β) => a • x }

@[instance_reducible]

instance Sum.instVAdd {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] : VAdd M (α ⊕ β)

Equations

• Sum.instVAdd = { vadd := fun (a : M) => Sum.map (fun (x : α) => a +ᵥ x) fun (x : β) => a +ᵥ x }

theorem Sum.smul_def {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] (a : M) (x : α ⊕ β) : a • x = Sum.map (fun (x : α) => a • x) (fun (x : β) => a • x) x

theorem Sum.vadd_def {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (x : α ⊕ β) : a +ᵥ x = Sum.map (fun (x : α) => a +ᵥ x) (fun (x : β) => a +ᵥ x) x

@[simp]

theorem Sum.smul_inl {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] (a : M) (b : α) : a • inl b = inl (a • b)

@[simp]

theorem Sum.vadd_inl {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (b : α) : a +ᵥ inl b = inl (a +ᵥ b)

@[simp]

theorem Sum.smul_inr {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] (a : M) (c : β) : a • inr c = inr (a • c)

@[simp]

theorem Sum.vadd_inr {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (c : β) : a +ᵥ inr c = inr (a +ᵥ c)

@[simp]

theorem Sum.smul_swap {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] (a : M) (x : α ⊕ β) : (a • x).swap = a • x.swap

@[simp]

theorem Sum.vadd_swap {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] (a : M) (x : α ⊕ β) : (a +ᵥ x).swap = a +ᵥ x.swap

instance Sum.instIsScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [SMul M N] [IsScalarTower M N α] [IsScalarTower M N β] : IsScalarTower M N (α ⊕ β)

instance Sum.instSMulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [SMul N α] [SMul N β] [SMulCommClass M N α] [SMulCommClass M N β] : SMulCommClass M N (α ⊕ β)

instance Sum.instVAddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [VAdd N α] [VAdd N β] [VAddCommClass M N α] [VAddCommClass M N β] : VAddCommClass M N (α ⊕ β)

instance Sum.instIsCentralScalar {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [SMul Mᵐᵒᵖ α] [SMul Mᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β] : IsCentralScalar M (α ⊕ β)

instance Sum.instIsCentralVAdd {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [VAdd Mᵃᵒᵖ α] [VAdd Mᵃᵒᵖ β] [IsCentralVAdd M α] [IsCentralVAdd M β] : IsCentralVAdd M (α ⊕ β)

instance Sum.FaithfulSMulLeft {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [FaithfulSMul M α] : FaithfulSMul M (α ⊕ β)

instance Sum.FaithfulVAddLeft {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [FaithfulVAdd M α] : FaithfulVAdd M (α ⊕ β)

instance Sum.FaithfulSMulRight {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [FaithfulSMul M β] : FaithfulSMul M (α ⊕ β)

instance Sum.FaithfulVAddRight {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [FaithfulVAdd M β] : FaithfulVAdd M (α ⊕ β)

@[instance_reducible]

instance Sum.instMulAction {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : Monoid M} [MulAction M α] [MulAction M β] : MulAction M (α ⊕ β)

Equations

• Sum.instMulAction = { toSMul := Sum.instSMul, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

instance Sum.instAddAction {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : AddMonoid M} [AddAction M α] [AddAction M β] : AddAction M (α ⊕ β)

Equations

• Sum.instAddAction = { toVAdd := Sum.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }