Documentation

Mathlib.Algebra.Group.Action.Sum

Sum instances for additive and multiplicative actions #

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

See also #

source
instance Sum.instSMul_mathlib {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] :
SMul M (α ⊕ β)
Equations
    source
    instance Sum.hasVAdd {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] :
    VAdd M (α ⊕ β)
    Equations
      source
      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
      source
      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
      source
      @[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)
      source
      @[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)
      source
      @[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)
      source
      @[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)
      source
      @[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
      source
      @[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
      source
      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 (α ⊕ β)
      source
      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 (α ⊕ β)
      source
      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 (α ⊕ β)
      source
      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 (α ⊕ β)
      source
      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 (α ⊕ β)
      source
      instance Sum.FaithfulSMulLeft {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [FaithfulSMul M α] :
      FaithfulSMul M (α ⊕ β)
      source
      instance Sum.FaithfulVAddLeft {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [FaithfulVAdd M α] :
      FaithfulVAdd M (α ⊕ β)
      source
      instance Sum.FaithfulSMulRight {M : Type u_1} {α : Type u_3} {β : Type u_4} [SMul M α] [SMul M β] [FaithfulSMul M β] :
      FaithfulSMul M (α ⊕ β)
      source
      instance Sum.FaithfulVAddRight {M : Type u_1} {α : Type u_3} {β : Type u_4} [VAdd M α] [VAdd M β] [FaithfulVAdd M β] :
      FaithfulVAdd M (α ⊕ β)
      source
      instance Sum.instMulAction {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : Monoid M} [MulAction M α] [MulAction M β] :
      MulAction M (α ⊕ β)
      Equations
        source
        instance Sum.instAddAction {M : Type u_1} {α : Type u_3} {β : Type u_4} {m : AddMonoid M} [AddAction M α] [AddAction M β] :
        AddAction M (α ⊕ β)
        Equations