Documentation

Mathlib.Algebra.Group.Action.Defs

Definitions of group actions #

This file defines a hierarchy of group action type-classes on top of the previously defined notation classes SMul and its additive version VAdd:

The hierarchy is extended further by Module, defined elsewhere.

Also provided are typeclasses for faithful and transitive actions, and typeclasses regarding the interaction of different group actions,

Notation #

Implementation details #

This file should avoid depending on other parts of GroupTheory, to avoid import cycles. More sophisticated lemmas belong in GroupTheory.GroupAction.

Tags #

group action

Faithful actions #

class FaithfulVAdd (G : Type u_11) (P : Type u_12) [VAdd G P] :

Typeclass for faithful actions.

  • eq_of_vadd_eq_vadd : ∀ {g₁ g₂ : G}, (∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p)g₁ = g₂

    Two elements g₁ and g₂ are equal whenever they act in the same way on all points.

Instances
    theorem FaithfulVAdd.eq_of_vadd_eq_vadd {G : Type u_11} {P : Type u_12} [VAdd G P] [self : FaithfulVAdd G P] {g₁ : G} {g₂ : G} :
    (∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p)g₁ = g₂

    Two elements g₁ and g₂ are equal whenever they act in the same way on all points.

    class FaithfulSMul (M : Type u_11) (α : Type u_12) [SMul M α] :

    Typeclass for faithful actions.

    • eq_of_smul_eq_smul : ∀ {m₁ m₂ : M}, (∀ (a : α), m₁ a = m₂ a)m₁ = m₂

      Two elements m₁ and m₂ are equal whenever they act in the same way on all points.

    Instances
      theorem FaithfulSMul.eq_of_smul_eq_smul {M : Type u_11} {α : Type u_12} [SMul M α] [self : FaithfulSMul M α] {m₁ : M} {m₂ : M} :
      (∀ (a : α), m₁ a = m₂ a)m₁ = m₂

      Two elements m₁ and m₂ are equal whenever they act in the same way on all points.

      theorem vadd_left_injective' {M : Type u_1} {α : Type u_7} [VAdd M α] [FaithfulVAdd M α] :
      Function.Injective fun (x : M) (x_1 : α) => x +ᵥ x_1
      theorem smul_left_injective' {M : Type u_1} {α : Type u_7} [SMul M α] [FaithfulSMul M α] :
      Function.Injective fun (x : M) (x_1 : α) => x x_1
      @[instance 910]
      instance Add.toVAdd (α : Type u_11) [Add α] :
      VAdd α α

      See also AddMonoid.toAddAction

      Equations
      @[instance 910]
      instance Mul.toSMul (α : Type u_11) [Mul α] :
      SMul α α

      See also Monoid.toMulAction and MulZeroClass.toSMulWithZero.

      Equations
      @[simp]
      theorem vadd_eq_add (α : Type u_11) [Add α] {a : α} {a' : α} :
      a +ᵥ a' = a + a'
      @[simp]
      theorem smul_eq_mul (α : Type u_11) [Mul α] {a : α} {a' : α} :
      a a' = a * a'

      AddMonoid.toAddAction is faithful on additive cancellative monoids.

      Equations
      • =

      Monoid.toMulAction is faithful on cancellative monoids.

      Equations
      • =
      class AddAction (G : Type u_11) (P : Type u_12) [AddMonoid G] extends VAdd :
      Type (max u_11 u_12)

      Type class for additive monoid actions.

      • vadd : GPP
      • zero_vadd : ∀ (p : P), 0 +ᵥ p = p

        Zero is a neutral element for +ᵥ

      • add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)

        Associativity of + and +ᵥ

      Instances
        theorem AddAction.zero_vadd {G : Type u_11} {P : Type u_12} [AddMonoid G] [self : AddAction G P] (p : P) :
        0 +ᵥ p = p

        Zero is a neutral element for +ᵥ

        theorem AddAction.add_vadd {G : Type u_11} {P : Type u_12} [AddMonoid G] [self : AddAction G P] (g₁ : G) (g₂ : G) (p : P) :
        g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)

        Associativity of + and +ᵥ

        theorem MulAction.ext {α : Type u_11} {β : Type u_12} :
        ∀ {inst : Monoid α} (x y : MulAction α β), SMul.smul = SMul.smulx = y
        theorem AddAction.ext {G : Type u_11} {P : Type u_12} :
        ∀ {inst : AddMonoid G} (x y : AddAction G P), VAdd.vadd = VAdd.vaddx = y
        theorem AddAction.ext_iff {G : Type u_11} {P : Type u_12} :
        ∀ {inst : AddMonoid G} (x y : AddAction G P), x = y VAdd.vadd = VAdd.vadd
        theorem MulAction.ext_iff {α : Type u_11} {β : Type u_12} :
        ∀ {inst : Monoid α} (x y : MulAction α β), x = y SMul.smul = SMul.smul
        class MulAction (α : Type u_11) (β : Type u_12) [Monoid α] extends SMul :
        Type (max u_11 u_12)

        Typeclass for multiplicative actions by monoids. This generalizes group actions.

        • smul : αββ
        • one_smul : ∀ (b : β), 1 b = b

          One is the neutral element for

        • mul_smul : ∀ (x y : α) (b : β), (x * y) b = x y b

          Associativity of and *

        Instances
          theorem MulAction.one_smul {α : Type u_11} {β : Type u_12} [Monoid α] [self : MulAction α β] (b : β) :
          1 b = b

          One is the neutral element for

          theorem MulAction.mul_smul {α : Type u_11} {β : Type u_12} [Monoid α] [self : MulAction α β] (x : α) (y : α) (b : β) :
          (x * y) b = x y b

          Associativity of and *

          (Pre)transitive action #

          M acts pretransitively on α if for any x y there is g such that g • x = y (or g +ᵥ x = y for an additive action). A transitive action should furthermore have α nonempty.

          In this section we define typeclasses MulAction.IsPretransitive and AddAction.IsPretransitive and provide MulAction.exists_smul_eq/AddAction.exists_vadd_eq, MulAction.surjective_smul/AddAction.surjective_vadd as public interface to access this property. We do not provide typeclasses *Action.IsTransitive; users should assume [MulAction.IsPretransitive M α] [Nonempty α] instead.

          class AddAction.IsPretransitive (M : Type u_11) (α : Type u_12) [VAdd M α] :

          M acts pretransitively on α if for any x y there is g such that g +ᵥ x = y. A transitive action should furthermore have α nonempty.

          • exists_vadd_eq : ∀ (x y : α), ∃ (g : M), g +ᵥ x = y

            There is g such that g +ᵥ x = y.

          Instances
            theorem AddAction.IsPretransitive.exists_vadd_eq {M : Type u_11} {α : Type u_12} [VAdd M α] [self : AddAction.IsPretransitive M α] (x : α) (y : α) :
            ∃ (g : M), g +ᵥ x = y

            There is g such that g +ᵥ x = y.

            class MulAction.IsPretransitive (M : Type u_11) (α : Type u_12) [SMul M α] :

            M acts pretransitively on α if for any x y there is g such that g • x = y. A transitive action should furthermore have α nonempty.

            • exists_smul_eq : ∀ (x y : α), ∃ (g : M), g x = y

              There is g such that g • x = y.

            Instances
              theorem MulAction.IsPretransitive.exists_smul_eq {M : Type u_11} {α : Type u_12} [SMul M α] [self : MulAction.IsPretransitive M α] (x : α) (y : α) :
              ∃ (g : M), g x = y

              There is g such that g • x = y.

              theorem AddAction.exists_vadd_eq (M : Type u_1) {α : Type u_7} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) (y : α) :
              ∃ (m : M), m +ᵥ x = y
              theorem MulAction.exists_smul_eq (M : Type u_1) {α : Type u_7} [SMul M α] [MulAction.IsPretransitive M α] (x : α) (y : α) :
              ∃ (m : M), m x = y
              theorem AddAction.surjective_vadd (M : Type u_1) {α : Type u_7} [VAdd M α] [AddAction.IsPretransitive M α] (x : α) :
              Function.Surjective fun (c : M) => c +ᵥ x
              theorem MulAction.surjective_smul (M : Type u_1) {α : Type u_7} [SMul M α] [MulAction.IsPretransitive M α] (x : α) :
              Function.Surjective fun (c : M) => c x

              The regular action of a group on itself is transitive.

              Equations
              • =

              The regular action of a group on itself is transitive.

              Equations
              • =

              Scalar tower and commuting actions #

              class VAddCommClass (M : Type u_11) (N : Type u_12) (α : Type u_13) [VAdd M α] [VAdd N α] :

              A typeclass mixin saying that two additive actions on the same space commute.

              • vadd_comm : ∀ (m : M) (n : N) (a : α), m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)

                +ᵥ is left commutative

              Instances
                theorem VAddCommClass.vadd_comm {M : Type u_11} {N : Type u_12} {α : Type u_13} [VAdd M α] [VAdd N α] [self : VAddCommClass M N α] (m : M) (n : N) (a : α) :
                m +ᵥ (n +ᵥ a) = n +ᵥ (m +ᵥ a)

                +ᵥ is left commutative

                class SMulCommClass (M : Type u_11) (N : Type u_12) (α : Type u_13) [SMul M α] [SMul N α] :

                A typeclass mixin saying that two multiplicative actions on the same space commute.

                • smul_comm : ∀ (m : M) (n : N) (a : α), m n a = n m a

                  is left commutative

                Instances
                  theorem SMulCommClass.smul_comm {M : Type u_11} {N : Type u_12} {α : Type u_13} [SMul M α] [SMul N α] [self : SMulCommClass M N α] (m : M) (n : N) (a : α) :
                  m n a = n m a

                  is left commutative

                  theorem VAddCommClass.symm (M : Type u_11) (N : Type u_12) (α : Type u_13) [VAdd M α] [VAdd N α] [VAddCommClass M N α] :

                  Commutativity of additive actions is a symmetric relation. This lemma can't be an instance because this would cause a loop in the instance search graph.

                  theorem SMulCommClass.symm (M : Type u_11) (N : Type u_12) (α : Type u_13) [SMul M α] [SMul N α] [SMulCommClass M N α] :

                  Commutativity of actions is a symmetric relation. This lemma can't be an instance because this would cause a loop in the instance search graph.

                  theorem Function.Injective.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd N α] [VAdd M β] [VAdd N β] [VAddCommClass M N β] {f : αβ} (hf : Function.Injective f) (h₁ : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (h₂ : ∀ (c : N) (x : α), f (c +ᵥ x) = c +ᵥ f x) :
                  theorem Function.Injective.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul N α] [SMul M β] [SMul N β] [SMulCommClass M N β] {f : αβ} (hf : Function.Injective f) (h₁ : ∀ (c : M) (x : α), f (c x) = c f x) (h₂ : ∀ (c : N) (x : α), f (c x) = c f x) :
                  theorem Function.Surjective.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd N α] [VAdd M β] [VAdd N β] [VAddCommClass M N α] {f : αβ} (hf : Function.Surjective f) (h₁ : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (h₂ : ∀ (c : N) (x : α), f (c +ᵥ x) = c +ᵥ f x) :
                  theorem Function.Surjective.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul N α] [SMul M β] [SMul N β] [SMulCommClass M N α] {f : αβ} (hf : Function.Surjective f) (h₁ : ∀ (c : M) (x : α), f (c x) = c f x) (h₂ : ∀ (c : N) (x : α), f (c x) = c f x) :
                  instance vaddCommClass_self (M : Type u_11) (α : Type u_12) [AddCommMonoid M] [AddAction M α] :
                  Equations
                  • =
                  instance smulCommClass_self (M : Type u_11) (α : Type u_12) [CommMonoid M] [MulAction M α] :
                  Equations
                  • =
                  class VAddAssocClass (M : Type u_11) (N : Type u_12) (α : Type u_13) [VAdd M N] [VAdd N α] [VAdd M α] :

                  An instance of VAddAssocClass M N α states that the additive action of M on α is determined by the additive actions of M on N and N on α.

                  • vadd_assoc : ∀ (x : M) (y : N) (z : α), x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)

                    Associativity of +ᵥ

                  Instances
                    theorem VAddAssocClass.vadd_assoc {M : Type u_11} {N : Type u_12} {α : Type u_13} [VAdd M N] [VAdd N α] [VAdd M α] [self : VAddAssocClass M N α] (x : M) (y : N) (z : α) :
                    x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)

                    Associativity of +ᵥ

                    class IsScalarTower (M : Type u_11) (N : Type u_12) (α : Type u_13) [SMul M N] [SMul N α] [SMul M α] :

                    An instance of IsScalarTower M N α states that the multiplicative action of M on α is determined by the multiplicative actions of M on N and N on α.

                    • smul_assoc : ∀ (x : M) (y : N) (z : α), (x y) z = x y z

                      Associativity of

                    Instances
                      theorem IsScalarTower.smul_assoc {M : Type u_11} {N : Type u_12} {α : Type u_13} [SMul M N] [SMul N α] [SMul M α] [self : IsScalarTower M N α] (x : M) (y : N) (z : α) :
                      (x y) z = x y z

                      Associativity of

                      @[simp]
                      theorem vadd_assoc {α : Type u_7} {M : Type u_11} {N : Type u_12} [VAdd M N] [VAdd N α] [VAdd M α] [VAddAssocClass M N α] (x : M) (y : N) (z : α) :
                      x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)
                      @[simp]
                      theorem smul_assoc {α : Type u_7} {M : Type u_11} {N : Type u_12} [SMul M N] [SMul N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : N) (z : α) :
                      (x y) z = x y z
                      instance AddSemigroup.isScalarTower {α : Type u_7} [AddSemigroup α] :
                      Equations
                      • =
                      instance Semigroup.isScalarTower {α : Type u_7} [Semigroup α] :
                      IsScalarTower α α α
                      Equations
                      • =
                      class IsCentralVAdd (M : Type u_11) (α : Type u_12) [VAdd M α] [VAdd Mᵃᵒᵖ α] :

                      A typeclass indicating that the right (aka AddOpposite) and left actions by M on α are equal, that is that M acts centrally on α. This can be thought of as a version of commutativity for +ᵥ.

                      • op_vadd_eq_vadd : ∀ (m : M) (a : α), AddOpposite.op m +ᵥ a = m +ᵥ a

                        The right and left actions of M on α are equal.

                      Instances
                        theorem IsCentralVAdd.op_vadd_eq_vadd {M : Type u_11} {α : Type u_12} [VAdd M α] [VAdd Mᵃᵒᵖ α] [self : IsCentralVAdd M α] (m : M) (a : α) :

                        The right and left actions of M on α are equal.

                        class IsCentralScalar (M : Type u_11) (α : Type u_12) [SMul M α] [SMul Mᵐᵒᵖ α] :

                        A typeclass indicating that the right (aka MulOpposite) and left actions by M on α are equal, that is that M acts centrally on α. This can be thought of as a version of commutativity for .

                        • op_smul_eq_smul : ∀ (m : M) (a : α), MulOpposite.op m a = m a

                          The right and left actions of M on α are equal.

                        Instances
                          @[simp]
                          theorem IsCentralScalar.op_smul_eq_smul {M : Type u_11} {α : Type u_12} [SMul M α] [SMul Mᵐᵒᵖ α] [self : IsCentralScalar M α] (m : M) (a : α) :

                          The right and left actions of M on α are equal.

                          theorem IsCentralVAdd.unop_vadd_eq_vadd {M : Type u_11} {α : Type u_12} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] (m : Mᵃᵒᵖ) (a : α) :
                          theorem IsCentralScalar.unop_smul_eq_smul {M : Type u_11} {α : Type u_12} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (m : Mᵐᵒᵖ) (a : α) :
                          @[instance 50]
                          instance VAddCommClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_7} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] [VAdd N α] [VAddCommClass M N α] :
                          Equations
                          • =
                          @[instance 50]
                          instance SMulCommClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [SMul N α] [SMulCommClass M N α] :
                          Equations
                          • =
                          @[instance 50]
                          instance VAddCommClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_7} [VAdd M α] [VAdd N α] [VAdd Nᵃᵒᵖ α] [IsCentralVAdd N α] [VAddCommClass M N α] :
                          Equations
                          • =
                          @[instance 50]
                          instance SMulCommClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] [SMul N α] [SMul Nᵐᵒᵖ α] [IsCentralScalar N α] [SMulCommClass M N α] :
                          Equations
                          • =
                          @[instance 50]
                          instance VAddAssocClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_7} [VAdd M α] [VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] [VAdd M N] [VAdd Mᵃᵒᵖ N] [IsCentralVAdd M N] [VAdd N α] [VAddAssocClass M N α] :
                          Equations
                          • =
                          @[instance 50]
                          instance IsScalarTower.op_left {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [SMul M N] [SMul Mᵐᵒᵖ N] [IsCentralScalar M N] [SMul N α] [IsScalarTower M N α] :
                          Equations
                          • =
                          @[instance 50]
                          instance VAddAssocClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_7} [VAdd M α] [VAdd M N] [VAdd N α] [VAdd Nᵃᵒᵖ α] [IsCentralVAdd N α] [VAddAssocClass M N α] :
                          Equations
                          • =
                          @[instance 50]
                          instance IsScalarTower.op_right {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] [SMul M N] [SMul N α] [SMul Nᵐᵒᵖ α] [IsCentralScalar N α] [IsScalarTower M N α] :
                          Equations
                          • =
                          def VAdd.comp.vadd {M : Type u_1} {N : Type u_2} {α : Type u_7} [VAdd M α] (g : NM) (n : N) (a : α) :
                          α

                          Auxiliary definition for VAdd.comp, AddAction.compHom, etc.

                          Equations
                          Instances For
                            def SMul.comp.smul {M : Type u_1} {N : Type u_2} {α : Type u_7} [SMul M α] (g : NM) (n : N) (a : α) :
                            α

                            Auxiliary definition for SMul.comp, MulAction.compHom, DistribMulAction.compHom, Module.compHom, etc.

                            Equations
                            Instances For
                              @[reducible]
                              def VAdd.comp {M : Type u_1} {N : Type u_2} (α : Type u_7) [VAdd M α] (g : NM) :
                              VAdd N α

                              An additive action of M on α and a function N → M induces an additive action of N on α.

                              Equations
                              Instances For
                                @[reducible]
                                def SMul.comp {M : Type u_1} {N : Type u_2} (α : Type u_7) [SMul M α] (g : NM) :
                                SMul N α

                                An action of M on α and a function N → M induces an action of N on α.

                                Equations
                                Instances For
                                  theorem VAdd.comp.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd M β] [VAdd α β] [VAddAssocClass M α β] (g : NM) :

                                  Given a tower of additive actions M → α → β, if we use SMul.comp to pull back both of M's actions by a map g : N → M, then we obtain a new tower of scalar actions N → α → β.

                                  This cannot be an instance because it can cause infinite loops whenever the SMul arguments are still metavariables.

                                  theorem SMul.comp.isScalarTower {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul M β] [SMul α β] [IsScalarTower M α β] (g : NM) :

                                  Given a tower of scalar actions M → α → β, if we use SMul.comp to pull back both of M's actions by a map g : N → M, then we obtain a new tower of scalar actions N → α → β.

                                  This cannot be an instance because it can cause infinite loops whenever the SMul arguments are still metavariables.

                                  theorem VAdd.comp.vaddCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd β α] [VAddCommClass M β α] (g : NM) :

                                  This cannot be an instance because it can cause infinite loops whenever the VAdd arguments are still metavariables.

                                  theorem SMul.comp.smulCommClass {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul β α] [SMulCommClass M β α] (g : NM) :

                                  This cannot be an instance because it can cause infinite loops whenever the SMul arguments are still metavariables.

                                  theorem VAdd.comp.vaddCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [VAdd M α] [VAdd β α] [VAddCommClass β M α] (g : NM) :

                                  This cannot be an instance because it can cause infinite loops whenever the VAdd arguments are still metavariables.

                                  theorem SMul.comp.smulCommClass' {M : Type u_1} {N : Type u_2} {α : Type u_7} {β : Type u_8} [SMul M α] [SMul β α] [SMulCommClass β M α] (g : NM) :

                                  This cannot be an instance because it can cause infinite loops whenever the SMul arguments are still metavariables.

                                  theorem add_vadd_comm {α : Type u_7} {β : Type u_8} [Add β] [VAdd α β] [VAddCommClass α β β] (s : α) (x : β) (y : β) :
                                  x + (s +ᵥ y) = s +ᵥ (x + y)
                                  theorem mul_smul_comm {α : Type u_7} {β : Type u_8} [Mul β] [SMul α β] [SMulCommClass α β β] (s : α) (x : β) (y : β) :
                                  x * s y = s (x * y)

                                  Note that the SMulCommClass α β β typeclass argument is usually satisfied by Algebra α β.

                                  theorem vadd_add_assoc {α : Type u_7} {β : Type u_8} [Add β] [VAdd α β] [VAddAssocClass α β β] (r : α) (x : β) (y : β) :
                                  r +ᵥ x + y = r +ᵥ (x + y)
                                  theorem smul_mul_assoc {α : Type u_7} {β : Type u_8} [Mul β] [SMul α β] [IsScalarTower α β β] (r : α) (x : β) (y : β) :
                                  r x * y = r (x * y)

                                  Note that the IsScalarTower α β β typeclass argument is usually satisfied by Algebra α β.

                                  theorem vadd_sub_assoc {α : Type u_7} {β : Type u_8} [SubNegMonoid β] [VAdd α β] [VAddAssocClass α β β] (r : α) (x : β) (y : β) :
                                  r +ᵥ x - y = r +ᵥ (x - y)
                                  theorem smul_div_assoc {α : Type u_7} {β : Type u_8} [DivInvMonoid β] [SMul α β] [IsScalarTower α β β] (r : α) (x : β) (y : β) :
                                  r x / y = r (x / y)

                                  Note that the IsScalarTower α β β typeclass argument is usually satisfied by Algebra α β.

                                  theorem vadd_vadd_vadd_comm {α : Type u_7} {β : Type u_8} {γ : Type u_9} {δ : Type u_10} [VAdd α β] [VAdd α γ] [VAdd β δ] [VAdd α δ] [VAdd γ δ] [VAddAssocClass α β δ] [VAddAssocClass α γ δ] [VAddCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) :
                                  a +ᵥ b +ᵥ (c +ᵥ d) = a +ᵥ c +ᵥ (b +ᵥ d)
                                  theorem smul_smul_smul_comm {α : Type u_7} {β : Type u_8} {γ : Type u_9} {δ : Type u_10} [SMul α β] [SMul α γ] [SMul β δ] [SMul α δ] [SMul γ δ] [IsScalarTower α β δ] [IsScalarTower α γ δ] [SMulCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) :
                                  (a b) c d = (a c) b d
                                  theorem AddCommute.vadd_right {M : Type u_1} {α : Type u_7} [VAdd M α] [Add α] [VAddCommClass M α α] [VAddAssocClass M α α] {a : α} {b : α} (h : AddCommute a b) (r : M) :
                                  theorem Commute.smul_right {M : Type u_1} {α : Type u_7} [SMul M α] [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a : α} {b : α} (h : Commute a b) (r : M) :
                                  Commute a (r b)
                                  theorem AddCommute.vadd_left {M : Type u_1} {α : Type u_7} [VAdd M α] [Add α] [VAddCommClass M α α] [VAddAssocClass M α α] {a : α} {b : α} (h : AddCommute a b) (r : M) :
                                  theorem Commute.smul_left {M : Type u_1} {α : Type u_7} [SMul M α] [Mul α] [SMulCommClass M α α] [IsScalarTower M α α] {a : α} {b : α} (h : Commute a b) (r : M) :
                                  Commute (r a) b
                                  theorem vadd_vadd {M : Type u_1} {α : Type u_7} [AddMonoid M] [AddAction M α] (a₁ : M) (a₂ : M) (b : α) :
                                  a₁ +ᵥ (a₂ +ᵥ b) = a₁ + a₂ +ᵥ b
                                  theorem smul_smul {M : Type u_1} {α : Type u_7} [Monoid M] [MulAction M α] (a₁ : M) (a₂ : M) (b : α) :
                                  a₁ a₂ b = (a₁ * a₂) b
                                  @[simp]
                                  theorem zero_vadd (M : Type u_1) {α : Type u_7} [AddMonoid M] [AddAction M α] (b : α) :
                                  0 +ᵥ b = b
                                  @[simp]
                                  theorem one_smul (M : Type u_1) {α : Type u_7} [Monoid M] [MulAction M α] (b : α) :
                                  1 b = b
                                  theorem zero_vadd_eq_id (M : Type u_1) {α : Type u_7} [AddMonoid M] [AddAction M α] :
                                  (fun (x : α) => 0 +ᵥ x) = id

                                  VAdd version of zero_add_eq_id

                                  theorem one_smul_eq_id (M : Type u_1) {α : Type u_7} [Monoid M] [MulAction M α] :
                                  (fun (x : α) => 1 x) = id

                                  SMul version of one_mul_eq_id

                                  theorem comp_vadd_left (M : Type u_1) {α : Type u_7} [AddMonoid M] [AddAction M α] (a₁ : M) (a₂ : M) :
                                  ((fun (x : α) => a₁ +ᵥ x) fun (x : α) => a₂ +ᵥ x) = fun (x : α) => a₁ + a₂ +ᵥ x

                                  VAdd version of comp_add_left

                                  theorem comp_smul_left (M : Type u_1) {α : Type u_7} [Monoid M] [MulAction M α] (a₁ : M) (a₂ : M) :
                                  ((fun (x : α) => a₁ x) fun (x : α) => a₂ x) = fun (x : α) => (a₁ * a₂) x

                                  SMul version of comp_mul_left

                                  theorem Function.Injective.addAction.proof_1 {M : Type u_2} {α : Type u_3} {β : Type u_1} [AddMonoid M] [AddAction M α] [VAdd M β] (f : βα) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) (x : β) :
                                  0 +ᵥ x = x
                                  @[reducible]
                                  def Function.Injective.addAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [AddMonoid M] [AddAction M α] [VAdd M β] (f : βα) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) :

                                  Pullback an additive action along an injective map respecting +ᵥ.

                                  Equations
                                  Instances For
                                    theorem Function.Injective.addAction.proof_2 {M : Type u_2} {α : Type u_3} {β : Type u_1} [AddMonoid M] [AddAction M α] [VAdd M β] (f : βα) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) (c₁ : M) (c₂ : M) (x : β) :
                                    c₁ + c₂ +ᵥ x = c₁ +ᵥ (c₂ +ᵥ x)
                                    @[reducible]
                                    def Function.Injective.mulAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [Monoid M] [MulAction M α] [SMul M β] (f : βα) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c x) = c f x) :

                                    Pullback a multiplicative action along an injective map respecting . See note [reducible non-instances].

                                    Equations
                                    Instances For
                                      @[reducible]
                                      def Function.Surjective.addAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [AddMonoid M] [AddAction M α] [VAdd M β] (f : αβ) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) :

                                      Pushforward an additive action along a surjective map respecting +ᵥ.

                                      Equations
                                      Instances For
                                        theorem Function.Surjective.addAction.proof_1 {M : Type u_2} {α : Type u_3} {β : Type u_1} [AddMonoid M] [AddAction M α] [VAdd M β] (f : αβ) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (y : β) :
                                        0 +ᵥ y = y
                                        theorem Function.Surjective.addAction.proof_2 {M : Type u_2} {α : Type u_3} {β : Type u_1} [AddMonoid M] [AddAction M α] [VAdd M β] (f : αβ) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (a : M) (a : M) (y : β) :
                                        a✝ + a +ᵥ y = a✝ +ᵥ (a +ᵥ y)
                                        @[reducible]
                                        def Function.Surjective.mulAction {M : Type u_1} {α : Type u_7} {β : Type u_8} [Monoid M] [MulAction M α] [SMul M β] (f : αβ) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c x) = c f x) :

                                        Pushforward a multiplicative action along a surjective map respecting . See note [reducible non-instances].

                                        Equations
                                        Instances For
                                          @[reducible]
                                          def Function.Surjective.addActionLeft {R : Type u_11} {S : Type u_12} {M : Type u_13} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) :

                                          Push forward the action of R on M along a compatible surjective map f : R →+ S.

                                          Equations
                                          Instances For
                                            theorem Function.Surjective.addActionLeft.proof_1 {R : Type u_3} {S : Type u_2} {M : Type u_1} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) (b : M) :
                                            0 +ᵥ b = b
                                            theorem Function.Surjective.addActionLeft.proof_2 {R : Type u_3} {S : Type u_2} {M : Type u_1} [AddMonoid R] [AddAction R M] [AddMonoid S] [VAdd S M] (f : R →+ S) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) (y₁ : S) (y₂ : S) (b : M) :
                                            y₁ + y₂ +ᵥ b = y₁ +ᵥ (y₂ +ᵥ b)
                                            @[reducible]
                                            def Function.Surjective.mulActionLeft {R : Type u_11} {S : Type u_12} {M : Type u_13} [Monoid R] [MulAction R M] [Monoid S] [SMul S M] (f : R →* S) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c x = c x) :

                                            Push forward the action of R on M along a compatible surjective map f : R →* S.

                                            See also Function.Surjective.distribMulActionLeft and Function.Surjective.moduleLeft.

                                            Equations
                                            Instances For
                                              theorem AddMonoid.toAddAction.proof_2 (M : Type u_1) [AddMonoid M] (a : M) (b : M) (c : M) :
                                              a + b + c = a + (b + c)
                                              theorem AddMonoid.toAddAction.proof_1 (M : Type u_1) [AddMonoid M] (a : M) :
                                              0 + a = a
                                              @[instance 910]
                                              instance AddMonoid.toAddAction (M : Type u_1) [AddMonoid M] :

                                              The regular action of a monoid on itself by left addition.

                                              This is promoted to an AddTorsor by addGroup_is_addTorsor.

                                              Equations
                                              @[instance 910]
                                              instance Monoid.toMulAction (M : Type u_1) [Monoid M] :

                                              The regular action of a monoid on itself by left multiplication.

                                              This is promoted to a module by Semiring.toModule.

                                              Equations
                                              instance VAddAssocClass.left (M : Type u_1) {α : Type u_7} [AddMonoid M] [AddAction M α] :
                                              Equations
                                              • =
                                              instance IsScalarTower.left (M : Type u_1) {α : Type u_7} [Monoid M] [MulAction M α] :
                                              Equations
                                              • =
                                              theorem vadd_add_vadd {M : Type u_1} {α : Type u_7} [AddMonoid M] [AddAction M α] [Add α] (r : M) (s : M) (x : α) (y : α) [VAddAssocClass M α α] [VAddCommClass M α α] :
                                              r +ᵥ x + (s +ᵥ y) = r + s +ᵥ (x + y)
                                              theorem smul_mul_smul {M : Type u_1} {α : Type u_7} [Monoid M] [MulAction M α] [Mul α] (r : M) (s : M) (x : α) (y : α) [IsScalarTower M α α] [SMulCommClass M α α] :
                                              r x * s y = (r * s) (x * y)

                                              Note that the IsScalarTower M α α and SMulCommClass M α α typeclass arguments are usually satisfied by Algebra M α.

                                              theorem smul_pow {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (r : M) (x : N) (n : ) :
                                              (r x) ^ n = r ^ n x ^ n
                                              @[simp]
                                              theorem neg_vadd_vadd {G : Type u_3} {α : Type u_7} [AddGroup G] [AddAction G α] (g : G) (a : α) :
                                              -g +ᵥ (g +ᵥ a) = a
                                              @[simp]
                                              theorem inv_smul_smul {G : Type u_3} {α : Type u_7} [Group G] [MulAction G α] (g : G) (a : α) :
                                              g⁻¹ g a = a
                                              @[simp]
                                              theorem vadd_neg_vadd {G : Type u_3} {α : Type u_7} [AddGroup G] [AddAction G α] (g : G) (a : α) :
                                              g +ᵥ (-g +ᵥ a) = a
                                              @[simp]
                                              theorem smul_inv_smul {G : Type u_3} {α : Type u_7} [Group G] [MulAction G α] (g : G) (a : α) :
                                              g g⁻¹ a = a
                                              theorem neg_vadd_eq_iff {G : Type u_3} {α : Type u_7} [AddGroup G] [AddAction G α] {g : G} {a : α} {b : α} :
                                              -g +ᵥ a = b a = g +ᵥ b
                                              theorem inv_smul_eq_iff {G : Type u_3} {α : Type u_7} [Group G] [MulAction G α] {g : G} {a : α} {b : α} :
                                              g⁻¹ a = b a = g b
                                              theorem eq_neg_vadd_iff {G : Type u_3} {α : Type u_7} [AddGroup G] [AddAction G α] {g : G} {a : α} {b : α} :
                                              a = -g +ᵥ b g +ᵥ a = b
                                              theorem eq_inv_smul_iff {G : Type u_3} {α : Type u_7} [Group G] [MulAction G α] {g : G} {a : α} {b : α} :
                                              a = g⁻¹ b g a = b
                                              @[simp]
                                              theorem Commute.smul_right_iff {G : Type u_3} {H : Type u_4} [Group G] [Mul H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] {g : G} {a : H} {b : H} :
                                              Commute a (g b) Commute a b
                                              @[simp]
                                              theorem Commute.smul_left_iff {G : Type u_3} {H : Type u_4} [Group G] [Mul H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] {g : G} {a : H} {b : H} :
                                              Commute (g a) b Commute a b
                                              theorem smul_inv {G : Type u_3} {H : Type u_4} [Group G] [Group H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] (g : G) (a : H) :
                                              theorem smul_zpow {G : Type u_3} {H : Type u_4} [Group G] [Group H] [MulAction G H] [SMulCommClass G H H] [IsScalarTower G H H] (g : G) (a : H) (n : ) :
                                              (g a) ^ n = g ^ n a ^ n
                                              theorem SMulCommClass.of_commMonoid (A : Type u_11) (B : Type u_12) (G : Type u_13) [CommMonoid G] [SMul A G] [SMul B G] [IsScalarTower A G G] [IsScalarTower B G G] :
                                              theorem AddAction.toFun.proof_1 (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] (y₁ : α) (y₂ : α) (H : (fun (y : α) (x : M) => x +ᵥ y) y₁ = (fun (y : α) (x : M) => x +ᵥ y) y₂) :
                                              y₁ = y₂
                                              def AddAction.toFun (M : Type u_1) (α : Type u_7) [AddMonoid M] [AddAction M α] :
                                              α Mα

                                              Embedding of α into functions M → α induced by an additive action of M on α.

                                              Equations
                                              Instances For
                                                def MulAction.toFun (M : Type u_1) (α : Type u_7) [Monoid M] [MulAction M α] :
                                                α Mα

                                                Embedding of α into functions M → α induced by a multiplicative action of M on α.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem AddAction.toFun_apply {M : Type u_1} {α : Type u_7} [AddMonoid M] [AddAction M α] (x : M) (y : α) :
                                                  (AddAction.toFun M α) y x = x +ᵥ y
                                                  @[simp]
                                                  theorem MulAction.toFun_apply {M : Type u_1} {α : Type u_7} [Monoid M] [MulAction M α] (x : M) (y : α) :
                                                  (MulAction.toFun M α) y x = x y
                                                  theorem AddAction.compHom.proof_1 {M : Type u_3} {N : Type u_2} (α : Type u_1) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) :
                                                  ∀ (x : α), 0 +ᵥ x = x
                                                  theorem AddAction.compHom.proof_2 {M : Type u_3} {N : Type u_2} (α : Type u_1) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) :
                                                  ∀ (x x_1 : N) (x_2 : α), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)
                                                  @[reducible]
                                                  def AddAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_7) [AddMonoid M] [AddAction M α] [AddMonoid N] (g : N →+ M) :

                                                  An additive action of M on α and an additive monoid homomorphism N → M induce an additive action of N on α.

                                                  See note [reducible non-instances].

                                                  Equations
                                                  Instances For
                                                    @[reducible]
                                                    def MulAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_7) [Monoid M] [MulAction M α] [Monoid N] (g : N →* M) :

                                                    A multiplicative action of M on α and a monoid homomorphism N → M induce a multiplicative action of N on α.

                                                    See note [reducible non-instances].

                                                    Equations
                                                    Instances For
                                                      theorem AddAction.compHom_vadd_def {E : Type u_11} {F : Type u_12} {G : Type u_13} [AddMonoid E] [AddMonoid F] [AddAction F G] (f : E →+ F) (a : E) (x : G) :
                                                      a +ᵥ x = f a +ᵥ x
                                                      theorem MulAction.compHom_smul_def {E : Type u_11} {F : Type u_12} {G : Type u_13} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
                                                      a x = f a x
                                                      theorem MulAction.isPretransitive_compHom {E : Type u_11} {F : Type u_12} {G : Type u_13} [Monoid E] [Monoid F] [MulAction F G] [MulAction.IsPretransitive F G] {f : E →* F} (hf : Function.Surjective f) :

                                                      If an action is transitive, then composing this action with a surjective homomorphism gives again a transitive action.

                                                      theorem AddAction.IsPretransitive.of_vadd_eq {M : Type u_11} {N : Type u_12} {α : Type u_13} [VAdd M α] [VAdd N α] [AddAction.IsPretransitive M α] (f : MN) (hf : ∀ {c : M} {x : α}, f c +ᵥ x = c +ᵥ x) :
                                                      theorem MulAction.IsPretransitive.of_smul_eq {M : Type u_11} {N : Type u_12} {α : Type u_13} [SMul M α] [SMul N α] [MulAction.IsPretransitive M α] (f : MN) (hf : ∀ {c : M} {x : α}, f c x = c x) :
                                                      theorem AddAction.IsPretransitive.of_compHom {M : Type u_11} {N : Type u_12} {α : Type u_13} [AddMonoid M] [AddMonoid N] [AddAction N α] (f : M →+ N) [h : AddAction.IsPretransitive M α] :
                                                      theorem MulAction.IsPretransitive.of_compHom {M : Type u_11} {N : Type u_12} {α : Type u_13} [Monoid M] [Monoid N] [MulAction N α] (f : M →* N) [h : MulAction.IsPretransitive M α] :
                                                      theorem vadd_zero_vadd {α : Type u_7} {M : Type u_11} (N : Type u_12) [AddMonoid N] [VAdd M N] [AddAction N α] [VAdd M α] [VAddAssocClass M N α] (x : M) (y : α) :
                                                      x +ᵥ 0 +ᵥ y = x +ᵥ y
                                                      theorem smul_one_smul {α : Type u_7} {M : Type u_11} (N : Type u_12) [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : α) :
                                                      (x 1) y = x y
                                                      theorem MulAction.IsPretransitive.of_isScalarTower (M : Type u_11) {N : Type u_12} {α : Type u_13} [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] [MulAction.IsPretransitive M α] :
                                                      @[simp]
                                                      theorem vadd_zero_add {M : Type u_11} {N : Type u_12} [AddZeroClass N] [VAdd M N] [VAddAssocClass M N N] (x : M) (y : N) :
                                                      x +ᵥ 0 + y = x +ᵥ y
                                                      @[simp]
                                                      theorem smul_one_mul {M : Type u_11} {N : Type u_12} [MulOneClass N] [SMul M N] [IsScalarTower M N N] (x : M) (y : N) :
                                                      x 1 * y = x y
                                                      @[simp]
                                                      theorem add_vadd_zero {M : Type u_11} {N : Type u_12} [AddZeroClass N] [VAdd M N] [VAddCommClass M N N] (x : M) (y : N) :
                                                      y + (x +ᵥ 0) = x +ᵥ y
                                                      @[simp]
                                                      theorem mul_smul_one {M : Type u_11} {N : Type u_12} [MulOneClass N] [SMul M N] [SMulCommClass M N N] (x : M) (y : N) :
                                                      y * x 1 = x y
                                                      theorem VAddAssocClass.of_vadd_zero_add {M : Type u_11} {N : Type u_12} [AddMonoid N] [VAdd M N] (h : ∀ (x : M) (y : N), x +ᵥ 0 + y = x +ᵥ y) :
                                                      theorem IsScalarTower.of_smul_one_mul {M : Type u_11} {N : Type u_12} [Monoid N] [SMul M N] (h : ∀ (x : M) (y : N), x 1 * y = x y) :
                                                      theorem VAddCommClass.of_add_vadd_zero {M : Type u_11} {N : Type u_12} [AddMonoid N] [VAdd M N] (H : ∀ (x : M) (y : N), y + (x +ᵥ 0) = x +ᵥ y) :
                                                      theorem SMulCommClass.of_mul_smul_one {M : Type u_11} {N : Type u_12} [Monoid N] [SMul M N] (H : ∀ (x : M) (y : N), y * x 1 = x y) :
                                                      theorem AddMonoidHom.vaddZeroHom.proof_2 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] (x : M) (y : M) :
                                                      { toFun := fun (x : M) => x +ᵥ 0, map_zero' := }.toFun (x + y) = { toFun := fun (x : M) => x +ᵥ 0, map_zero' := }.toFun x + { toFun := fun (x : M) => x +ᵥ 0, map_zero' := }.toFun y
                                                      theorem AddMonoidHom.vaddZeroHom.proof_1 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddZeroClass N] [AddAction M N] :
                                                      0 +ᵥ 0 = 0
                                                      def AddMonoidHom.vaddZeroHom {M : Type u_11} {N : Type u_12} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] :
                                                      M →+ N

                                                      If the additive action of M on N is compatible with addition on N, then fun x ↦ x +ᵥ 0 is an additive monoid homomorphism from M to N.

                                                      Equations
                                                      • AddMonoidHom.vaddZeroHom = { toFun := fun (x : M) => x +ᵥ 0, map_zero' := , map_add' := }
                                                      Instances For
                                                        @[simp]
                                                        theorem AddMonoidHom.vaddZeroHom_apply {M : Type u_11} {N : Type u_12} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] (x : M) :
                                                        AddMonoidHom.vaddZeroHom x = x +ᵥ 0
                                                        @[simp]
                                                        theorem MonoidHom.smulOneHom_apply {M : Type u_11} {N : Type u_12} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] (x : M) :
                                                        MonoidHom.smulOneHom x = x 1
                                                        def MonoidHom.smulOneHom {M : Type u_11} {N : Type u_12} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] :
                                                        M →* N

                                                        If the multiplicative action of M on N is compatible with multiplication on N, then fun x ↦ x • 1 is a monoid homomorphism from M to N.

                                                        Equations
                                                        • MonoidHom.smulOneHom = { toFun := fun (x : M) => x 1, map_one' := , map_mul' := }
                                                        Instances For
                                                          theorem addMonoidHomEquivAddActionIsScalarTower.proof_3 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] :
                                                          ∀ (x : { _inst : AddAction M N // VAddAssocClass M N N }), (fun (f : M →+ N) => AddAction.compHom N f, ) ((fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => addMonoidHomEquivAddActionIsScalarTower.match_1 M N (fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => M →+ N) x fun (val : AddAction M N) (property : VAddAssocClass M N N) => AddMonoidHom.vaddZeroHom) x) = x
                                                          abbrev addMonoidHomEquivAddActionIsScalarTower.match_2 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] (motive : { _inst : AddAction M N // VAddAssocClass M N N }Prop) :
                                                          ∀ (x : { _inst : AddAction M N // VAddAssocClass M N N }), (∀ (val : AddAction M N) (property : VAddAssocClass M N N), motive val, property)motive x
                                                          Equations
                                                          • =
                                                          Instances For
                                                            abbrev addMonoidHomEquivAddActionIsScalarTower.match_1 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] (motive : { _inst : AddAction M N // VAddAssocClass M N N }Sort u_3) :
                                                            (x : { _inst : AddAction M N // VAddAssocClass M N N }) → ((val : AddAction M N) → (property : VAddAssocClass M N N) → motive val, property)motive x
                                                            Equations
                                                            Instances For
                                                              def addMonoidHomEquivAddActionIsScalarTower (M : Type u_11) (N : Type u_12) [AddMonoid M] [AddMonoid N] :
                                                              (M →+ N) { _inst : AddAction M N // VAddAssocClass M N N }

                                                              A monoid homomorphism between two additive monoids M and N can be equivalently specified by an additive action of M on N that is compatible with the addition on N.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                theorem addMonoidHomEquivAddActionIsScalarTower.proof_2 (M : Type u_1) (N : Type u_2) [AddMonoid M] [AddMonoid N] (f : M →+ N) :
                                                                (fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => addMonoidHomEquivAddActionIsScalarTower.match_1 M N (fun (x : { _inst : AddAction M N // VAddAssocClass M N N }) => M →+ N) x fun (val : AddAction M N) (property : VAddAssocClass M N N) => AddMonoidHom.vaddZeroHom) ((fun (f : M →+ N) => AddAction.compHom N f, ) f) = f
                                                                def monoidHomEquivMulActionIsScalarTower (M : Type u_11) (N : Type u_12) [Monoid M] [Monoid N] :
                                                                (M →* N) { _inst : MulAction M N // IsScalarTower M N N }

                                                                A monoid homomorphism between two monoids M and N can be equivalently specified by a multiplicative action of M on N that is compatible with the multiplication on N.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  def Function.End (α : Type u_7) :
                                                                  Type u_7

                                                                  The monoid of endomorphisms.

                                                                  Note that this is generalized by CategoryTheory.End to categories other than Type u.

                                                                  Equations
                                                                  Instances For
                                                                    instance instMonoidEnd (α : Type u_7) :
                                                                    Equations
                                                                    instance instInhabitedEnd (α : Type u_7) :
                                                                    Equations

                                                                    The tautological action by Function.End α on α.

                                                                    This is generalized to bundled endomorphisms by:

                                                                    • Equiv.Perm.applyMulAction
                                                                    • AddMonoid.End.applyDistribMulAction
                                                                    • AddMonoid.End.applyModule
                                                                    • AddAut.applyDistribMulAction
                                                                    • MulAut.applyMulDistribMulAction
                                                                    • LinearEquiv.applyDistribMulAction
                                                                    • LinearMap.applyModule
                                                                    • RingHom.applyMulSemiringAction
                                                                    • RingAut.applyMulSemiringAction
                                                                    • AlgEquiv.applyMulSemiringAction
                                                                    Equations
                                                                    @[simp]
                                                                    theorem Function.End.smul_def {α : Type u_7} (f : Function.End α) (a : α) :
                                                                    f a = f a
                                                                    theorem Function.End.mul_def {α : Type u_7} (f : Function.End α) (g : Function.End α) :
                                                                    f * g = f g
                                                                    theorem Function.End.one_def {α : Type u_7} :
                                                                    1 = id

                                                                    Function.End.applyMulAction is faithful.

                                                                    Equations
                                                                    • =
                                                                    def MulAction.toEndHom {M : Type u_1} {α : Type u_7} [Monoid M] [MulAction M α] :

                                                                    The monoid hom representing a monoid action.

                                                                    When M is a group, see MulAction.toPermHom.

                                                                    Equations
                                                                    • MulAction.toEndHom = { toFun := fun (x : M) (x_1 : α) => x x_1, map_one' := , map_mul' := }
                                                                    Instances For
                                                                      @[reducible, inline]
                                                                      abbrev MulAction.ofEndHom {M : Type u_1} {α : Type u_7} [Monoid M] (f : M →* Function.End α) :

                                                                      The monoid action induced by a monoid hom to Function.End α

                                                                      See note [reducible non-instances].

                                                                      Equations
                                                                      Instances For

                                                                        Additive, Multiplicative #

                                                                        instance Additive.vadd {α : Type u_7} {β : Type u_8} [SMul α β] :
                                                                        VAdd (Additive α) β
                                                                        Equations
                                                                        • Additive.vadd = { vadd := fun (a : Additive α) (x : β) => Additive.toMul a x }
                                                                        instance Multiplicative.smul {α : Type u_7} {β : Type u_8} [VAdd α β] :
                                                                        Equations
                                                                        • Multiplicative.smul = { smul := fun (a : Multiplicative α) (x : β) => Multiplicative.toAdd a +ᵥ x }
                                                                        @[simp]
                                                                        theorem toMul_smul {α : Type u_7} {β : Type u_8} [SMul α β] (a : Additive α) (b : β) :
                                                                        Additive.toMul a b = a +ᵥ b
                                                                        @[simp]
                                                                        theorem ofMul_vadd {α : Type u_7} {β : Type u_8} [SMul α β] (a : α) (b : β) :
                                                                        Additive.ofMul a +ᵥ b = a b
                                                                        @[simp]
                                                                        theorem toAdd_vadd {α : Type u_7} {β : Type u_8} [VAdd α β] (a : Multiplicative α) (b : β) :
                                                                        Multiplicative.toAdd a +ᵥ b = a b
                                                                        @[simp]
                                                                        theorem ofAdd_smul {α : Type u_7} {β : Type u_8} [VAdd α β] (a : α) (b : β) :
                                                                        Multiplicative.ofAdd a b = a +ᵥ b
                                                                        instance Additive.addAction {α : Type u_7} {β : Type u_8} [Monoid α] [MulAction α β] :
                                                                        Equations
                                                                        instance Multiplicative.mulAction {α : Type u_7} {β : Type u_8} [AddMonoid α] [AddAction α β] :
                                                                        Equations
                                                                        Equations
                                                                        • =
                                                                        instance Additive.vaddCommClass {α : Type u_7} {β : Type u_8} {γ : Type u_9} [SMul α γ] [SMul β γ] [SMulCommClass α β γ] :
                                                                        Equations
                                                                        • =
                                                                        instance Multiplicative.smulCommClass {α : Type u_7} {β : Type u_8} {γ : Type u_9} [VAdd α γ] [VAdd β γ] [VAddCommClass α β γ] :
                                                                        Equations
                                                                        • =

                                                                        The tautological additive action by Additive (Function.End α) on α.

                                                                        Equations
                                                                        • AddAction.functionEnd = inferInstance
                                                                        def AddAction.toEndHom {M : Type u_1} {α : Type u_7} [AddMonoid M] [AddAction M α] :

                                                                        The additive monoid hom representing an additive monoid action.

                                                                        When M is a group, see AddAction.toPermHom.

                                                                        Equations
                                                                        • AddAction.toEndHom = MonoidHom.toAdditive'' MulAction.toEndHom
                                                                        Instances For
                                                                          @[reducible, inline]
                                                                          abbrev AddAction.ofEndHom {M : Type u_1} {α : Type u_7} [AddMonoid M] (f : M →+ Additive (Function.End α)) :

                                                                          The additive action induced by a hom to Additive (Function.End α)

                                                                          See note [reducible non-instances].

                                                                          Equations
                                                                          Instances For