Sum instances for additive and multiplicative actions

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

See also

• GroupTheory.GroupAction.Option
• GroupTheory.GroupAction.Pi
• GroupTheory.GroupAction.Prod
• GroupTheory.GroupAction.Sigma

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

Equations

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• (_ : IsScalarTower M N (α ⊕ β)) = (_ : IsScalarTower M N (α ⊕ β))

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

Equations

• (_ : VAddCommClass M N (α ⊕ β)) = (_ : VAddCommClass M N (α ⊕ β))

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

Equations

• (_ : SMulCommClass M N (α ⊕ β)) = (_ : SMulCommClass M N (α ⊕ β))

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

Equations

• (_ : IsCentralVAdd M (α ⊕ β)) = (_ : IsCentralVAdd M (α ⊕ β))

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

Equations

• (_ : IsCentralScalar M (α ⊕ β)) = (_ : IsCentralScalar M (α ⊕ β))

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

Equations

• (_ : FaithfulVAdd M (α ⊕ β)) = (_ : FaithfulVAdd M (α ⊕ β))

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

Equations

• (_ : FaithfulSMul M (α ⊕ β)) = (_ : FaithfulSMul M (α ⊕ β))

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

Equations

• (_ : FaithfulVAdd M (α ⊕ β)) = (_ : FaithfulVAdd M (α ⊕ β))

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

Equations

• (_ : FaithfulSMul M (α ⊕ β)) = (_ : FaithfulSMul M (α ⊕ β))

theorem Sum.instAddActionSum.proof_1 {M : Type u_3} {α : Type u_1} {β : Type u_2} {m : AddMonoid M} [AddAction M α] [AddAction M β] (x : α ⊕ β) : 0 +ᵥ x = x

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

Equations

• Sum.instAddActionSum = AddAction.mk (_ : ∀ (x : α ⊕ β), 0 +ᵥ x = x) (_ : ∀ (a b : M) (x : α ⊕ β), a + b +ᵥ x = a +ᵥ (b +ᵥ x))

theorem Sum.instAddActionSum.proof_2 {M : Type u_3} {α : Type u_1} {β : Type u_2} {m : AddMonoid M} [AddAction M α] [AddAction M β] (a : M) (b : M) (x : α ⊕ β) : a + b +ᵥ x = a +ᵥ (b +ᵥ x)

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

Equations

• Sum.instMulActionSum = MulAction.mk (_ : ∀ (x : α ⊕ β), 1 • x = x) (_ : ∀ (a b : M) (x : α ⊕ β), (a * b) • x = a • b • x)