Documentation

Mathlib.GroupTheory.GroupAction.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_1) (P : Type u_2) [inst : VAdd G P] :
  • Two elements g₁ and g₂ are equal whenever they act in the same way on all points.

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

Typeclass for faithful actions.

Instances
    class FaithfulSMul (M : Type u_1) (α : Type u_2) [inst : SMul M α] :
    • Two elements m₁ and m₂ are equal whenever they act in the same way on all points.

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

    Typeclass for faithful actions.

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

      See also AddMonoid.toAddAction

      Equations
      instance Mul.toSMul (α : Type u_1) [inst : Mul α] :
      SMul α α

      See also Monoid.toMulAction and MulZeroClass.toSMulWithZero.

      Equations
      @[simp]
      theorem vadd_eq_add (α : Type u_1) [inst : Add α] {a : α} {a' : α} :
      a +ᵥ a' = a + a'
      @[simp]
      theorem smul_eq_mul (α : Type u_1) [inst : Mul α] {a : α} {a' : α} :
      a a' = a * a'
      class AddAction (G : Type u_1) (P : Type u_2) [inst : AddMonoid G] extends VAdd :
      Type (maxu_1u_2)
      • Zero is a neutral element for +ᵥ

        zero_vadd : ∀ (p : P), 0 +ᵥ p = p
      • Associativity of + and +ᵥ

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

      Type class for additive monoid actions.

      Instances
        theorem MulAction.ext {α : Type u_1} {β : Type u_2} :
        ∀ {inst : Monoid α} (x y : MulAction α β), SMul.smul = SMul.smulx = y
        theorem AddAction.ext_iff {G : Type u_1} {P : Type u_2} :
        ∀ {inst : AddMonoid G} (x y : AddAction G P), x = y VAdd.vadd = VAdd.vadd
        theorem MulAction.ext_iff {α : Type u_1} {β : Type u_2} :
        ∀ {inst : Monoid α} (x y : MulAction α β), x = y SMul.smul = SMul.smul
        theorem AddAction.ext {G : Type u_1} {P : Type u_2} :
        ∀ {inst : AddMonoid G} (x y : AddAction G P), VAdd.vadd = VAdd.vaddx = y
        class MulAction (α : Type u_1) (β : Type u_2) [inst : Monoid α] extends SMul :
        Type (maxu_1u_2)
        • One is the neutral element for

          one_smul : ∀ (b : β), 1 b = b
        • Associativity of and *

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

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

        Instances

          (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_1) (α : Type u_2) [inst : VAdd M α] :
          • There is g such that g +ᵥ x = y.

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

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

          Instances
            class MulAction.IsPretransitive (M : Type u_1) (α : Type u_2) [inst : SMul M α] :
            • There is g such that g • x = y.

              exists_smul_eq : ∀ (x y : α), g, g x = y

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

            Instances
              theorem AddAction.exists_vadd_eq (M : Type u_1) {α : Type u_2} [inst : VAdd M α] [inst : AddAction.IsPretransitive M α] (x : α) (y : α) :
              m, m +ᵥ x = y
              theorem MulAction.exists_smul_eq (M : Type u_1) {α : Type u_2} [inst : SMul M α] [inst : MulAction.IsPretransitive M α] (x : α) (y : α) :
              m, m x = y
              theorem AddAction.surjective_vadd (M : Type u_1) {α : Type u_2} [inst : VAdd M α] [inst : AddAction.IsPretransitive M α] (x : α) :
              theorem MulAction.surjective_smul (M : Type u_1) {α : Type u_2} [inst : SMul M α] [inst : MulAction.IsPretransitive M α] (x : α) :

              The regular action of a group on itself is transitive.

              Equations

              Scalar tower and commuting actions #

              class VAddCommClass (M : Type u_1) (N : Type u_2) (α : Type u_3) [inst : VAdd M α] [inst : VAdd N α] :
              • +ᵥ is left commutative

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

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

              Instances
                class SMulCommClass (M : Type u_1) (N : Type u_2) (α : Type u_3) [inst : SMul M α] [inst : SMul N α] :
                • is left commutative

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

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

                Instances
                  theorem VAddCommClass.symm (M : Type u_1) (N : Type u_2) (α : Type u_3) [inst : VAdd M α] [inst : VAdd N α] [inst : 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_1) (N : Type u_2) (α : Type u_3) [inst : SMul M α] [inst : SMul N α] [inst : 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.

                  instance vaddCommClass_self (M : Type u_1) (α : Type u_2) [inst : AddCommMonoid M] [inst : AddAction M α] :
                  Equations
                  def vaddCommClass_self.proof_1 (M : Type u_1) (α : Type u_2) [inst : AddCommMonoid M] [inst : AddAction M α] :
                  Equations
                  instance smulCommClass_self (M : Type u_1) (α : Type u_2) [inst : CommMonoid M] [inst : MulAction M α] :
                  Equations
                  class VAddAssocClass (M : Type u_1) (N : Type u_2) (α : Type u_3) [inst : VAdd M N] [inst : VAdd N α] [inst : VAdd M α] :
                  • Associativity of +ᵥ

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

                  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 α.

                  Instances
                    class IsScalarTower (M : Type u_1) (N : Type u_2) (α : Type u_3) [inst : SMul M N] [inst : SMul N α] [inst : SMul M α] :
                    • Associativity of

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

                    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 α.

                    Instances
                      @[simp]
                      theorem vadd_assoc {α : Type u_3} {M : Type u_1} {N : Type u_2} [inst : VAdd M N] [inst : VAdd N α] [inst : VAdd M α] [inst : VAddAssocClass M N α] (x : M) (y : N) (z : α) :
                      x +ᵥ y +ᵥ z = x +ᵥ (y +ᵥ z)
                      @[simp]
                      theorem smul_assoc {α : Type u_3} {M : Type u_1} {N : Type u_2} [inst : SMul M N] [inst : SMul N α] [inst : SMul M α] [inst : IsScalarTower M N α] (x : M) (y : N) (z : α) :
                      (x y) z = x y z
                      Equations
                      class IsCentralVAdd (M : Type u_1) (α : Type u_2) [inst : VAdd M α] [inst : VAdd Mᵃᵒᵖ α] :
                      • The right and left actions of M on α are equal.

                        op_vadd_eq_vadd : ∀ (m : M) (a : α), { unop := m } +ᵥ a = m +ᵥ a

                      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 +ᵥ.

                      Instances
                        class IsCentralScalar (M : Type u_1) (α : Type u_2) [inst : SMul M α] [inst : SMul Mᵐᵒᵖ α] :
                        • The right and left actions of M on α are equal.

                          op_smul_eq_smul : ∀ (m : M) (a : α), { unop := m } a = m a

                        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 .

                        Instances
                          theorem IsCentralVAdd.unop_vadd_eq_vadd {M : Type u_1} {α : Type u_2} [inst : VAdd M α] [inst : VAdd Mᵃᵒᵖ α] [inst : IsCentralVAdd M α] (m : Mᵃᵒᵖ) (a : α) :
                          m.unop +ᵥ a = m +ᵥ a
                          theorem IsCentralScalar.unop_smul_eq_smul {M : Type u_1} {α : Type u_2} [inst : SMul M α] [inst : SMul Mᵐᵒᵖ α] [inst : IsCentralScalar M α] (m : Mᵐᵒᵖ) (a : α) :
                          m.unop a = m a
                          instance VAddCommClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst : VAdd Mᵃᵒᵖ α] [inst : IsCentralVAdd M α] [inst : VAdd N α] [inst : VAddCommClass M N α] :
                          Equations
                          def VAddCommClass.op_left.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst : VAdd Mᵃᵒᵖ α] [inst : IsCentralVAdd M α] [inst : VAdd N α] [inst : VAddCommClass M N α] :
                          Equations
                          instance SMulCommClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst : SMul Mᵐᵒᵖ α] [inst : IsCentralScalar M α] [inst : SMul N α] [inst : SMulCommClass M N α] :
                          Equations
                          def VAddCommClass.op_right.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst : VAdd N α] [inst : VAdd Nᵃᵒᵖ α] [inst : IsCentralVAdd N α] [inst : VAddCommClass M N α] :
                          Equations
                          instance VAddCommClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst : VAdd N α] [inst : VAdd Nᵃᵒᵖ α] [inst : IsCentralVAdd N α] [inst : VAddCommClass M N α] :
                          Equations
                          instance SMulCommClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst : SMul N α] [inst : SMul Nᵐᵒᵖ α] [inst : IsCentralScalar N α] [inst : SMulCommClass M N α] :
                          Equations
                          instance VAddAssocClass.op_left {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst : VAdd Mᵃᵒᵖ α] [inst : IsCentralVAdd M α] [inst : VAdd M N] [inst : VAdd Mᵃᵒᵖ N] [inst : IsCentralVAdd M N] [inst : VAdd N α] [inst : VAddAssocClass M N α] :
                          Equations
                          def VAddAssocClass.op_left.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst : VAdd Mᵃᵒᵖ α] [inst : IsCentralVAdd M α] [inst : VAdd M N] [inst : VAdd Mᵃᵒᵖ N] [inst : IsCentralVAdd M N] [inst : VAdd N α] [inst : VAddAssocClass M N α] :
                          Equations
                          instance IsScalarTower.op_left {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst : SMul Mᵐᵒᵖ α] [inst : IsCentralScalar M α] [inst : SMul M N] [inst : SMul Mᵐᵒᵖ N] [inst : IsCentralScalar M N] [inst : SMul N α] [inst : IsScalarTower M N α] :
                          Equations
                          def VAddAssocClass.op_right.proof_1 {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst : VAdd M N] [inst : VAdd N α] [inst : VAdd Nᵃᵒᵖ α] [inst : IsCentralVAdd N α] [inst : VAddAssocClass M N α] :
                          Equations
                          instance VAddAssocClass.op_right {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] [inst : VAdd M N] [inst : VAdd N α] [inst : VAdd Nᵃᵒᵖ α] [inst : IsCentralVAdd N α] [inst : VAddAssocClass M N α] :
                          Equations
                          instance IsScalarTower.op_right {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst : SMul M N] [inst : SMul N α] [inst : SMul Nᵐᵒᵖ α] [inst : IsCentralScalar N α] [inst : IsScalarTower M N α] :
                          Equations
                          def VAdd.comp.vadd {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M α] (g : NM) (n : N) (a : α) :
                          α

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

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

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

                          Equations
                          def VAdd.comp {M : Type u_1} {N : Type u_2} (α : Type u_3) [inst : 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
                          def SMul.comp {M : Type u_1} {N : Type u_2} (α : Type u_3) [inst : SMul M α] (g : NM) :
                          SMul N α

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

                          See note [reducible non-instances]. Since this is reducible, we make sure to go via SMul.comp.smul to prevent typeclass inference unfolding too far.

                          Equations
                          theorem VAdd.comp.isScalarTower {M : Type u_1} {N : Type u_4} {α : Type u_3} {β : Type u_2} [inst : VAdd M α] [inst : VAdd M β] [inst : VAdd α β] [inst : 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_4} {α : Type u_3} {β : Type u_2} [inst : SMul M α] [inst : SMul M β] [inst : SMul α β] [inst : 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_3} {N : Type u_4} {α : Type u_2} {β : Type u_1} [inst : VAdd M α] [inst : VAdd β α] [inst : 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_3} {N : Type u_4} {α : Type u_2} {β : Type u_1} [inst : SMul M α] [inst : SMul β α] [inst : 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_3} {N : Type u_4} {α : Type u_2} {β : Type u_1} [inst : VAdd M α] [inst : VAdd β α] [inst : VAddCommClass β M α] (g : NM) :

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

                          theorem SMul.comp.smulCommClass' {M : Type u_3} {N : Type u_4} {α : Type u_2} {β : Type u_1} [inst : SMul M α] [inst : SMul β α] [inst : 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_2} {β : Type u_1} [inst : Add β] [inst : VAdd α β] [inst : VAddCommClass α β β] (s : α) (x : β) (y : β) :
                          x + (s +ᵥ y) = s +ᵥ (x + y)
                          theorem mul_smul_comm {α : Type u_2} {β : Type u_1} [inst : Mul β] [inst : SMul α β] [inst : 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_2} {β : Type u_1} [inst : Add β] [inst : VAdd α β] [inst : VAddAssocClass α β β] (r : α) (x : β) (y : β) :
                          r +ᵥ x + y = r +ᵥ (x + y)
                          theorem smul_mul_assoc {α : Type u_2} {β : Type u_1} [inst : Mul β] [inst : SMul α β] [inst : 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_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : VAdd α β] [inst : VAdd α γ] [inst : VAdd β δ] [inst : VAdd α δ] [inst : VAdd γ δ] [inst : VAddAssocClass α β δ] [inst : VAddAssocClass α γ δ] [inst : VAddCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) :
                          a +ᵥ b +ᵥ (c +ᵥ d) = a +ᵥ c +ᵥ (b +ᵥ d)
                          theorem smul_smul_smul_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : SMul α β] [inst : SMul α γ] [inst : SMul β δ] [inst : SMul α δ] [inst : SMul γ δ] [inst : IsScalarTower α β δ] [inst : IsScalarTower α γ δ] [inst : SMulCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) :
                          (a b) c d = (a c) b d
                          theorem AddCommute.vadd_right {M : Type u_2} {α : Type u_1} [inst : VAdd M α] [inst : Add α] [inst : VAddCommClass M α α] [inst : VAddAssocClass M α α] {a : α} {b : α} (h : AddCommute a b) (r : M) :
                          theorem Commute.smul_right {M : Type u_2} {α : Type u_1} [inst : SMul M α] [inst : Mul α] [inst : SMulCommClass M α α] [inst : IsScalarTower M α α] {a : α} {b : α} (h : Commute a b) (r : M) :
                          Commute a (r b)
                          theorem AddCommute.vadd_left {M : Type u_2} {α : Type u_1} [inst : VAdd M α] [inst : Add α] [inst : VAddCommClass M α α] [inst : VAddAssocClass M α α] {a : α} {b : α} (h : AddCommute a b) (r : M) :
                          theorem Commute.smul_left {M : Type u_2} {α : Type u_1} [inst : SMul M α] [inst : Mul α] [inst : SMulCommClass M α α] [inst : IsScalarTower M α α] {a : α} {b : α} (h : Commute a b) (r : M) :
                          Commute (r a) b
                          theorem ite_vadd {M : Type u_2} {α : Type u_1} [inst : VAdd M α] (p : Prop) [inst : Decidable p] (a₁ : M) (a₂ : M) (b : α) :
                          (if p then a₁ else a₂) +ᵥ b = if p then a₁ +ᵥ b else a₂ +ᵥ b
                          theorem ite_smul {M : Type u_2} {α : Type u_1} [inst : SMul M α] (p : Prop) [inst : Decidable p] (a₁ : M) (a₂ : M) (b : α) :
                          (if p then a₁ else a₂) b = if p then a₁ b else a₂ b
                          theorem vadd_ite {M : Type u_2} {α : Type u_1} [inst : VAdd M α] (p : Prop) [inst : Decidable p] (a : M) (b₁ : α) (b₂ : α) :
                          (a +ᵥ if p then b₁ else b₂) = if p then a +ᵥ b₁ else a +ᵥ b₂
                          theorem smul_ite {M : Type u_2} {α : Type u_1} [inst : SMul M α] (p : Prop) [inst : Decidable p] (a : M) (b₁ : α) (b₂ : α) :
                          (a if p then b₁ else b₂) = if p then a b₁ else a b₂
                          theorem vadd_vadd {M : Type u_2} {α : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] (a₁ : M) (a₂ : M) (b : α) :
                          a₁ +ᵥ (a₂ +ᵥ b) = a₁ + a₂ +ᵥ b
                          theorem smul_smul {M : Type u_2} {α : Type u_1} [inst : Monoid M] [inst : MulAction M α] (a₁ : M) (a₂ : M) (b : α) :
                          a₁ a₂ b = (a₁ * a₂) b
                          @[simp]
                          theorem zero_vadd (M : Type u_2) {α : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] (b : α) :
                          0 +ᵥ b = b
                          @[simp]
                          theorem one_smul (M : Type u_2) {α : Type u_1} [inst : Monoid M] [inst : MulAction M α] (b : α) :
                          1 b = b
                          theorem zero_vadd_eq_id (M : Type u_2) {α : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] :
                          (fun x x_1 => x +ᵥ x_1) 0 = id

                          VAdd version of zero_add_eq_id

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

                          SMul version of one_mul_eq_id

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

                          VAdd version of comp_add_left

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

                          SMul version of comp_mul_left

                          def Function.Injective.addAction.proof_2 {M : Type u_2} {α : Type u_3} {β : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] [inst : 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)
                          Equations
                          def Function.Injective.addAction {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddMonoid M] [inst : AddAction M α] [inst : 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
                          def Function.Injective.addAction.proof_1 {M : Type u_2} {α : Type u_3} {β : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] [inst : VAdd M β] (f : βα) (hf : Function.Injective f) (smul : ∀ (c : M) (x : β), f (c +ᵥ x) = c +ᵥ f x) (x : β) :
                          0 +ᵥ x = x
                          Equations
                          def Function.Injective.mulAction {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid M] [inst : MulAction M α] [inst : 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
                          def Function.Surjective.addAction.proof_1 {M : Type u_2} {α : Type u_3} {β : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] [inst : VAdd M β] (f : αβ) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (y : β) :
                          0 +ᵥ y = y
                          Equations
                          def Function.Surjective.addAction {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddMonoid M] [inst : AddAction M α] [inst : 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
                          def Function.Surjective.addAction.proof_2 {M : Type u_2} {α : Type u_3} {β : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] [inst : VAdd M β] (f : αβ) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x) (c₁ : M) (c₂ : M) (y : β) :
                          c₁ + c₂ +ᵥ y = c₁ +ᵥ (c₂ +ᵥ y)
                          Equations
                          def Function.Surjective.mulAction {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid M] [inst : MulAction M α] [inst : 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
                          def Function.Surjective.addActionLeft {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : AddMonoid R] [inst : AddAction R M] [inst : AddMonoid S] [inst : 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
                          def Function.Surjective.addActionLeft.proof_2 {R : Type u_3} {S : Type u_2} {M : Type u_1} [inst : AddMonoid R] [inst : AddAction R M] [inst : AddMonoid S] [inst : 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)
                          Equations
                          • (_ : ∀ (y₁ y₂ : S) (b : M), y₁ + y₂ +ᵥ b = y₁ +ᵥ (y₂ +ᵥ b)) = (_ : ∀ (y₁ y₂ : S) (b : M), y₁ + y₂ +ᵥ b = y₁ +ᵥ (y₂ +ᵥ b))
                          def Function.Surjective.addActionLeft.proof_1 {R : Type u_3} {S : Type u_2} {M : Type u_1} [inst : AddMonoid R] [inst : AddAction R M] [inst : AddMonoid S] [inst : VAdd S M] (f : R →+ S) (hsmul : ∀ (c : R) (x : M), f c +ᵥ x = c +ᵥ x) (b : M) :
                          0 +ᵥ b = b
                          Equations
                          def Function.Surjective.mulActionLeft {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Monoid R] [inst : MulAction R M] [inst : Monoid S] [inst : 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
                          instance AddMonoid.toAddAction (M : Type u_1) [inst : AddMonoid M] :

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

                          This is promoted to an AddTorsor by addGroup_is_addTorsor.

                          Equations
                          def AddMonoid.toAddAction.proof_1 (M : Type u_1) [inst : AddMonoid M] (a : M) (b : M) (c : M) :
                          a + b + c = a + (b + c)
                          Equations
                          • (_ : ∀ (a b c : M), a + b + c = a + (b + c)) = (_ : ∀ (a b c : M), a + b + c = a + (b + c))
                          instance Monoid.toMulAction (M : Type u_1) [inst : 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_2} [inst : AddMonoid M] [inst : AddAction M α] :
                          Equations
                          def VAddAssocClass.left.proof_1 (M : Type u_1) {α : Type u_2} [inst : AddMonoid M] [inst : AddAction M α] :
                          Equations
                          instance IsScalarTower.left (M : Type u_1) {α : Type u_2} [inst : Monoid M] [inst : MulAction M α] :
                          Equations
                          theorem vadd_add_vadd {M : Type u_2} {α : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] [inst : Add α] (r : M) (s : M) (x : α) (y : α) [inst : VAddAssocClass M α α] [inst : VAddCommClass M α α] :
                          r +ᵥ x + (s +ᵥ y) = r + s +ᵥ (x + y)
                          theorem smul_mul_smul {M : Type u_2} {α : Type u_1} [inst : Monoid M] [inst : MulAction M α] [inst : Mul α] (r : M) (s : M) (x : α) (y : α) [inst : IsScalarTower M α α] [inst : 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 α.

                          def AddAction.toFun.proof_1 (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst : AddAction M α] (y₁ : α) (y₂ : α) (H : (fun y x => x +ᵥ y) y₁ = (fun y x => x +ᵥ y) y₂) :
                          y₁ = y₂
                          Equations
                          • (_ : y₁ = y₂) = (_ : y₁ = y₂)
                          def AddAction.toFun (M : Type u_1) (α : Type u_2) [inst : AddMonoid M] [inst : AddAction M α] :
                          α Mα

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

                          Equations
                          • AddAction.toFun M α = { toFun := fun y x => x +ᵥ y, inj' := (_ : ∀ (y₁ y₂ : α), (fun y x => x +ᵥ y) y₁ = (fun y x => x +ᵥ y) y₂y₁ = y₂) }
                          def MulAction.toFun (M : Type u_1) (α : Type u_2) [inst : Monoid M] [inst : MulAction M α] :
                          α Mα

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

                          Equations
                          • MulAction.toFun M α = { toFun := fun y x => x y, inj' := (_ : ∀ (y₁ y₂ : α), (fun y x => x y) y₁ = (fun y x => x y) y₂y₁ = y₂) }
                          @[simp]
                          theorem AddAction.toFun_apply {M : Type u_2} {α : Type u_1} [inst : AddMonoid M] [inst : AddAction M α] (x : M) (y : α) :
                          ↑(AddAction.toFun M α) y x = x +ᵥ y
                          @[simp]
                          theorem MulAction.toFun_apply {M : Type u_2} {α : Type u_1} [inst : Monoid M] [inst : MulAction M α] (x : M) (y : α) :
                          ↑(MulAction.toFun M α) y x = x y
                          def AddAction.compHom.proof_1 {M : Type u_3} {N : Type u_2} (α : Type u_1) [inst : AddMonoid M] [inst : AddAction M α] [inst : AddMonoid N] (g : N →+ M) :
                          ∀ (x : α), 0 +ᵥ x = x
                          Equations
                          def AddAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_3) [inst : AddMonoid M] [inst : AddAction M α] [inst : 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
                          def AddAction.compHom.proof_2 {M : Type u_3} {N : Type u_2} (α : Type u_1) [inst : AddMonoid M] [inst : AddAction M α] [inst : AddMonoid N] (g : N →+ M) :
                          ∀ (x x_1 : N) (x_2 : α), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)
                          Equations
                          def MulAction.compHom {M : Type u_1} {N : Type u_2} (α : Type u_3) [inst : Monoid M] [inst : MulAction M α] [inst : 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
                          theorem vadd_zero_vadd {α : Type u_3} {M : Type u_1} (N : Type u_2) [inst : AddMonoid N] [inst : VAdd M N] [inst : AddAction N α] [inst : VAdd M α] [inst : VAddAssocClass M N α] (x : M) (y : α) :
                          x +ᵥ 0 +ᵥ y = x +ᵥ y
                          theorem smul_one_smul {α : Type u_3} {M : Type u_1} (N : Type u_2) [inst : Monoid N] [inst : SMul M N] [inst : MulAction N α] [inst : SMul M α] [inst : IsScalarTower M N α] (x : M) (y : α) :
                          (x 1) y = x y
                          @[simp]
                          theorem vadd_zero_add {M : Type u_1} {N : Type u_2} [inst : AddZeroClass N] [inst : VAdd M N] [inst : VAddAssocClass M N N] (x : M) (y : N) :
                          x +ᵥ 0 + y = x +ᵥ y
                          @[simp]
                          theorem smul_one_mul {M : Type u_1} {N : Type u_2} [inst : MulOneClass N] [inst : SMul M N] [inst : IsScalarTower M N N] (x : M) (y : N) :
                          x 1 * y = x y
                          @[simp]
                          theorem add_vadd_zero {M : Type u_1} {N : Type u_2} [inst : AddZeroClass N] [inst : VAdd M N] [inst : VAddCommClass M N N] (x : M) (y : N) :
                          y + (x +ᵥ 0) = x +ᵥ y
                          @[simp]
                          theorem mul_smul_one {M : Type u_1} {N : Type u_2} [inst : MulOneClass N] [inst : SMul M N] [inst : SMulCommClass M N N] (x : M) (y : N) :
                          y * x 1 = x y
                          theorem VAddAssocClass.of_vadd_zero_add {M : Type u_1} {N : Type u_2} [inst : AddMonoid N] [inst : VAdd M N] (h : ∀ (x : M) (y : N), x +ᵥ 0 + y = x +ᵥ y) :
                          theorem IsScalarTower.of_smul_one_mul {M : Type u_1} {N : Type u_2} [inst : Monoid N] [inst : SMul M N] (h : ∀ (x : M) (y : N), x 1 * y = x y) :
                          theorem VAddCommClass.of_add_vadd_zero {M : Type u_1} {N : Type u_2} [inst : AddMonoid N] [inst : VAdd M N] (H : ∀ (x : M) (y : N), y + (x +ᵥ 0) = x +ᵥ y) :
                          theorem SMulCommClass.of_mul_smul_one {M : Type u_1} {N : Type u_2} [inst : Monoid N] [inst : SMul M N] (H : ∀ (x : M) (y : N), y * x 1 = x y) :
                          def vaddZeroHom {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] [inst : AddAction M N] [inst : 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
                          • One or more equations did not get rendered due to their size.
                          def vaddZeroHom.proof_2 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] [inst : AddAction M N] [inst : VAddAssocClass M N N] (x : M) (y : M) :
                          ZeroHom.toFun { toFun := fun x => x +ᵥ 0, map_zero' := (_ : 0 +ᵥ 0 = 0) } (x + y) = ZeroHom.toFun { toFun := fun x => x +ᵥ 0, map_zero' := (_ : 0 +ᵥ 0 = 0) } x + ZeroHom.toFun { toFun := fun x => x +ᵥ 0, map_zero' := (_ : 0 +ᵥ 0 = 0) } y
                          Equations
                          • One or more equations did not get rendered due to their size.
                          def vaddZeroHom.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] [inst : AddAction M N] :
                          0 +ᵥ 0 = 0
                          Equations
                          @[simp]
                          theorem smulOneHom_apply {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] [inst : MulAction M N] [inst : IsScalarTower M N N] (x : M) :
                          smulOneHom x = x 1
                          @[simp]
                          theorem vaddZeroHom_apply {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] [inst : AddAction M N] [inst : VAddAssocClass M N N] (x : M) :
                          vaddZeroHom x = x +ᵥ 0
                          def smulOneHom {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] [inst : MulAction M N] [inst : 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
                          • One or more equations did not get rendered due to their size.
                          class SMulZeroClass (M : Type u_1) (A : Type u_2) [inst : Zero A] extends SMul :
                          Type (maxu_1u_2)
                          • Multiplying 0 by a scalar gives 0

                            smul_zero : ∀ (a : M), a 0 = 0

                          Typeclass for scalar multiplication that preserves 0 on the right.

                          Instances
                            @[simp]
                            theorem smul_zero {M : Type u_2} {A : Type u_1} [inst : Zero A] [inst : SMulZeroClass M A] (a : M) :
                            a 0 = 0
                            def Function.Injective.smulZeroClass {M : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Zero A] [inst : SMulZeroClass M A] [inst : Zero B] [inst : SMul M B] (f : ZeroHom B A) (hf : Function.Injective f) (smul : ∀ (c : M) (x : B), f (c x) = c f x) :

                            Pullback a zero-preserving scalar multiplication along an injective zero-preserving map. See note [reducible non-instances].

                            Equations
                            def ZeroHom.smulZeroClass {M : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Zero A] [inst : SMulZeroClass M A] [inst : Zero B] [inst : SMul M B] (f : ZeroHom A B) (smul : ∀ (c : M) (x : A), f (c x) = c f x) :

                            Pushforward a zero-preserving scalar multiplication along a zero-preserving map. See note [reducible non-instances].

                            Equations
                            def Function.Surjective.smulZeroClassLeft {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Zero M] [inst : SMulZeroClass R M] [inst : SMul S M] (f : RS) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c x = c x) :

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

                            See also Function.Surjective.distribMulActionLeft.

                            Equations
                            def SMulZeroClass.compFun {M : Type u_1} {N : Type u_2} (A : Type u_3) [inst : Zero A] [inst : SMulZeroClass M A] (f : NM) :

                            Compose a SMulZeroClass with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

                            Equations
                            @[simp]
                            theorem SMulZeroClass.toZeroHom_apply {M : Type u_1} (A : Type u_2) [inst : Zero A] [inst : SMulZeroClass M A] (x : M) :
                            ∀ (x : A), ↑(SMulZeroClass.toZeroHom A x) x = (fun x x_1 => x x_1) x x
                            def SMulZeroClass.toZeroHom {M : Type u_1} (A : Type u_2) [inst : Zero A] [inst : SMulZeroClass M A] (x : M) :

                            Each element of the scalars defines a zero-preserving map.

                            Equations
                            theorem DistribSMul.ext_iff {M : Type u_1} {A : Type u_2} :
                            ∀ {inst : AddZeroClass A} (x y : DistribSMul M A), x = y SMul.smul = SMul.smul
                            theorem DistribSMul.ext {M : Type u_1} {A : Type u_2} :
                            ∀ {inst : AddZeroClass A} (x y : DistribSMul M A), SMul.smul = SMul.smulx = y
                            class DistribSMul (M : Type u_1) (A : Type u_2) [inst : AddZeroClass A] extends SMulZeroClass :
                            Type (maxu_1u_2)
                            • Scalar multiplication distributes across addition

                              smul_add : ∀ (a : M) (x y : A), a (x + y) = a x + a y

                            Typeclass for scalar multiplication that preserves 0 and + on the right.

                            This is exactly DistribMulAction without the MulAction part.

                            Instances
                              theorem smul_add {M : Type u_2} {A : Type u_1} [inst : AddZeroClass A] [inst : DistribSMul M A] (a : M) (b₁ : A) (b₂ : A) :
                              a (b₁ + b₂) = a b₁ + a b₂
                              def Function.Injective.distribSMul {M : Type u_1} {A : Type u_2} {B : Type u_3} [inst : AddZeroClass A] [inst : DistribSMul M A] [inst : AddZeroClass B] [inst : SMul M B] (f : B →+ A) (hf : Function.Injective f) (smul : ∀ (c : M) (x : B), f (c x) = c f x) :

                              Pullback a distributive scalar multiplication along an injective additive monoid homomorphism. See note [reducible non-instances].

                              Equations
                              def Function.Surjective.distribSMul {M : Type u_1} {A : Type u_2} {B : Type u_3} [inst : AddZeroClass A] [inst : DistribSMul M A] [inst : AddZeroClass B] [inst : SMul M B] (f : A →+ B) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : A), f (c x) = c f x) :

                              Pushforward a distributive scalar multiplication along a surjective additive monoid homomorphism. See note [reducible non-instances].

                              Equations
                              def Function.Surjective.distribSMulLeft {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : AddZeroClass M] [inst : DistribSMul R M] [inst : SMul S M] (f : RS) (hf : Function.Surjective f) (hsmul : ∀ (c : R) (x : M), f c x = c x) :

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

                              See also Function.Surjective.distribMulActionLeft.

                              Equations
                              def DistribSMul.compFun {M : Type u_1} {N : Type u_2} (A : Type u_3) [inst : AddZeroClass A] [inst : DistribSMul M A] (f : NM) :

                              Compose a DistribSMul with a function, with scalar multiplication f r' • m. See note [reducible non-instances].

                              Equations
                              @[simp]
                              theorem DistribSMul.toAddMonoidHom_apply {M : Type u_1} (A : Type u_2) [inst : AddZeroClass A] [inst : DistribSMul M A] (x : M) :
                              ∀ (x : A), ↑(DistribSMul.toAddMonoidHom A x) x = (fun x x_1 => x x_1) x x
                              def DistribSMul.toAddMonoidHom {M : Type u_1} (A : Type u_2) [inst : AddZeroClass A] [inst : DistribSMul M A] (x : M) :
                              A →+ A

                              Each element of the scalars defines a additive monoid homomorphism.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              theorem DistribMulAction.ext_iff {M : Type u_1} {A : Type u_2} :
                              ∀ {inst : Monoid M} {inst_1 : AddMonoid A} (x y : DistribMulAction M A), x = y SMul.smul = SMul.smul
                              theorem DistribMulAction.ext {M : Type u_1} {A : Type u_2} :
                              ∀ {inst : Monoid M} {inst_1 : AddMonoid A} (x y : DistribMulAction M A), SMul.smul = SMul.smulx = y
                              class DistribMulAction (M : Type u_1) (A : Type u_2) [inst : Monoid M] [inst : AddMonoid A] extends MulAction :
                              Type (maxu_1u_2)
                              • Multiplying 0 by a scalar gives 0

                                smul_zero : ∀ (a : M), a 0 = 0
                              • Scalar multiplication distributes across addition

                                smul_add : ∀ (a : M) (x y : A), a (x + y) = a x + a y

                              Typeclass for multiplicative actions on additive structures. This generalizes group modules.

                              Instances
                                instance DistribMulAction.toDistribSMul {M : Type u_1} {A : Type u_2} [inst : Monoid M] [inst : AddMonoid A] [inst : DistribMulAction M A] :
                                Equations

                                Since Lean 3 does not have definitional eta for structures, we have to make sure that the definition of DistribMulAction.toDistribSMul was done correctly, and the two paths from DistribMulAction to SMul are indeed definitionally equal.

                                def Function.Injective.distribMulAction {M : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid M] [inst : AddMonoid A] [inst : DistribMulAction M A] [inst : AddMonoid B] [inst : SMul M B] (f : B →+ A) (hf : Function.Injective f) (smul : ∀ (c : M) (x : B), f (c x) = c f x) :

                                Pullback a distributive multiplicative action along an injective additive monoid homomorphism. See note [reducible non-instances].

                                Equations
                                • One or more equations did not get rendered due to their size.
                                def Function.Surjective.distribMulAction {M : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid M] [inst : AddMonoid A] [inst : DistribMulAction M A] [inst : AddMonoid B] [inst : SMul M B] (f : A →+ B) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : A), f (c x) = c f x) :

                                Pushforward a distributive multiplicative action along a surjective additive monoid homomorphism. See note [reducible non-instances].

                                Equations
                                • One or more equations did not get rendered due to their size.
                                def Function.Surjective.distribMulActionLeft {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Monoid R] [inst : AddMonoid M] [inst : DistribMulAction R M] [inst : Monoid S] [inst : 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.mulActionLeft and Function.Surjective.moduleLeft.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                def DistribMulAction.compHom {M : Type u_1} {N : Type u_2} (A : Type u_3) [inst : Monoid M] [inst : AddMonoid A] [inst : DistribMulAction M A] [inst : Monoid N] (f : N →* M) :

                                Compose a DistribMulAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[simp]
                                theorem DistribMulAction.toAddMonoidHom_apply {M : Type u_1} (A : Type u_2) [inst : Monoid M] [inst : AddMonoid A] [inst : DistribMulAction M A] (x : M) :
                                ∀ (x : A), ↑(DistribMulAction.toAddMonoidHom A x) x = x x
                                def DistribMulAction.toAddMonoidHom {M : Type u_1} (A : Type u_2) [inst : Monoid M] [inst : AddMonoid A] [inst : DistribMulAction M A] (x : M) :
                                A →+ A

                                Each element of the monoid defines a additive monoid homomorphism.

                                Equations
                                @[simp]
                                theorem DistribMulAction.toAddMonoidEnd_apply (M : Type u_1) (A : Type u_2) [inst : Monoid M] [inst : AddMonoid A] [inst : DistribMulAction M A] (x : M) :
                                def DistribMulAction.toAddMonoidEnd (M : Type u_1) (A : Type u_2) [inst : Monoid M] [inst : AddMonoid A] [inst : DistribMulAction M A] :

                                Each element of the monoid defines an additive monoid homomorphism.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[simp]
                                theorem smul_neg {M : Type u_2} {A : Type u_1} [inst : Monoid M] [inst : AddGroup A] [inst : DistribMulAction M A] (r : M) (x : A) :
                                r -x = -(r x)
                                theorem smul_sub {M : Type u_2} {A : Type u_1} [inst : Monoid M] [inst : AddGroup A] [inst : DistribMulAction M A] (r : M) (x : A) (y : A) :
                                r (x - y) = r x - r y
                                theorem MulDistribMulAction.ext_iff {M : Type u_1} {A : Type u_2} :
                                ∀ {inst : Monoid M} {inst_1 : Monoid A} (x y : MulDistribMulAction M A), x = y SMul.smul = SMul.smul
                                theorem MulDistribMulAction.ext {M : Type u_1} {A : Type u_2} :
                                ∀ {inst : Monoid M} {inst_1 : Monoid A} (x y : MulDistribMulAction M A), SMul.smul = SMul.smulx = y
                                class MulDistribMulAction (M : Type u_1) (A : Type u_2) [inst : Monoid M] [inst : Monoid A] extends MulAction :
                                Type (maxu_1u_2)
                                • Distributivity of across *

                                  smul_mul : ∀ (r : M) (x y : A), r (x * y) = r x * r y
                                • Multiplying 1 by a scalar gives 1

                                  smul_one : ∀ (r : M), r 1 = 1

                                Typeclass for multiplicative actions on multiplicative structures. This generalizes conjugation actions.

                                Instances
                                  theorem smul_mul' {M : Type u_2} {A : Type u_1} [inst : Monoid M] [inst : Monoid A] [inst : MulDistribMulAction M A] (a : M) (b₁ : A) (b₂ : A) :
                                  a (b₁ * b₂) = a b₁ * a b₂
                                  def Function.Injective.mulDistribMulAction {M : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid M] [inst : Monoid A] [inst : MulDistribMulAction M A] [inst : Monoid B] [inst : SMul M B] (f : B →* A) (hf : Function.Injective f) (smul : ∀ (c : M) (x : B), f (c x) = c f x) :

                                  Pullback a multiplicative distributive multiplicative action along an injective monoid homomorphism. See note [reducible non-instances].

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  def Function.Surjective.mulDistribMulAction {M : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid M] [inst : Monoid A] [inst : MulDistribMulAction M A] [inst : Monoid B] [inst : SMul M B] (f : A →* B) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : A), f (c x) = c f x) :

                                  Pushforward a multiplicative distributive multiplicative action along a surjective monoid homomorphism. See note [reducible non-instances].

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  def MulDistribMulAction.compHom {M : Type u_1} {N : Type u_2} (A : Type u_3) [inst : Monoid M] [inst : Monoid A] [inst : MulDistribMulAction M A] [inst : Monoid N] (f : N →* M) :

                                  Compose a MulDistribMulAction with a MonoidHom, with action f r' • m. See note [reducible non-instances].

                                  Equations
                                  def MulDistribMulAction.toMonoidHom {M : Type u_1} (A : Type u_2) [inst : Monoid M] [inst : Monoid A] [inst : MulDistribMulAction M A] (r : M) :
                                  A →* A

                                  Scalar multiplication by r as a MonoidHom.

                                  Equations
                                  @[simp]
                                  theorem MulDistribMulAction.toMonoidHom_apply {M : Type u_2} {A : Type u_1} [inst : Monoid M] [inst : Monoid A] [inst : MulDistribMulAction M A] (r : M) (x : A) :
                                  @[simp]
                                  theorem MulDistribMulAction.toMonoidEnd_apply (M : Type u_1) (A : Type u_2) [inst : Monoid M] [inst : Monoid A] [inst : MulDistribMulAction M A] (r : M) :
                                  def MulDistribMulAction.toMonoidEnd (M : Type u_1) (A : Type u_2) [inst : Monoid M] [inst : Monoid A] [inst : MulDistribMulAction M A] :

                                  Each element of the monoid defines a monoid homomorphism.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  @[simp]
                                  theorem smul_inv' {M : Type u_2} {A : Type u_1} [inst : Monoid M] [inst : Group A] [inst : MulDistribMulAction M A] (r : M) (x : A) :
                                  r x⁻¹ = (r x)⁻¹
                                  theorem smul_div' {M : Type u_2} {A : Type u_1} [inst : Monoid M] [inst : Group A] [inst : MulDistribMulAction M A] (r : M) (x : A) (y : A) :
                                  r (x / y) = r x / r y
                                  def Function.End (α : Type u_1) :
                                  Type u_1

                                  The monoid of endomorphisms.

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

                                  Equations
                                  instance instMonoidEnd (α : Type u_1) :
                                  Equations
                                  instance instInhabitedEnd (α : Type u_1) :
                                  Equations

                                  The tautological action by Function.End α on α.

                                  This is generalized to bundled endomorphisms by:

                                  Equations
                                  @[simp]
                                  theorem Function.End.smul_def {α : Type u_1} (f : Function.End α) (a : α) :
                                  f a = f a

                                  The tautological action by AddMonoid.End α on α.

                                  This generalizes Function.End.applyMulAction.

                                  Equations
                                  • AddMonoid.End.applyDistribMulAction = DistribMulAction.mk (_ : ∀ (f : α →+ α), f 0 = 0) (_ : ∀ (f : α →+ α) (a b : α), f (a + b) = f a + f b)
                                  @[simp]
                                  theorem AddMonoid.End.smul_def {α : Type u_1} [inst : AddMonoid α] (f : AddMonoid.End α) (a : α) :
                                  f a = f a
                                  def MulAction.toEndHom {M : Type u_1} {α : Type u_2} [inst : Monoid M] [inst : MulAction M α] :

                                  The monoid hom representing a monoid action.

                                  When M is a group, see MulAction.toPermHom.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  def MulAction.ofEndHom {M : Type u_1} {α : Type u_2} [inst : Monoid M] (f : M →* Function.End α) :

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

                                  See note [reducible non-instances].

                                  Equations

                                  additive, multiplicative #

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

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

                                  Equations
                                  • AddAction.functionEnd = inferInstance
                                  def AddAction.toEndHom {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst : 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
                                  def AddAction.ofEndHom {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] (f : M →+ Additive (Function.End α)) :

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

                                  See note [reducible non-instances].

                                  Equations