Documentation

Mathlib.Algebra.GroupWithZero.Action.Prod

Prod instances for multiplicative actions with zero #

This file defines instances for MulActionWithZero and related structures on α × β

See also #

source
theorem Prod.smul_zero_mk {M : Type u_1} {β : Type u_4} [SMul M β] {α : Type u_5} [Monoid M] [AddMonoid α] [DistribMulAction M α] (a : M) (c : β) :
a • (0, c) = (0, a • c)
source
theorem Prod.smul_mk_zero {M : Type u_1} {α : Type u_3} [SMul M α] {β : Type u_5} [Monoid M] [AddMonoid β] [DistribMulAction M β] (a : M) (b : α) :
a • (b, 0) = (a • b, 0)
source
instance Prod.smulZeroClass {R : Type u_5} {M : Type u_6} {N : Type u_7} [Zero M] [Zero N] [SMulZeroClass R M] [SMulZeroClass R N] :
SMulZeroClass R (M × N)
Equations
    source
    instance Prod.distribSMul {R : Type u_5} {M : Type u_6} {N : Type u_7} [AddZeroClass M] [AddZeroClass N] [DistribSMul R M] [DistribSMul R N] :
    DistribSMul R (M × N)
    Equations
      source
      instance Prod.distribMulAction {M : Type u_1} {N : Type u_2} {R : Type u_5} [Monoid R] [AddMonoid M] [AddMonoid N] [DistribMulAction R M] [DistribMulAction R N] :
      DistribMulAction R (M × N)
      Equations
        source
        instance Prod.mulDistribMulAction {M : Type u_1} {N : Type u_2} {R : Type u_5} [Monoid R] [Monoid M] [Monoid N] [MulDistribMulAction R M] [MulDistribMulAction R N] :
        MulDistribMulAction R (M × N)
        Equations
          source
          instance Prod.smulWithZero {M : Type u_1} {N : Type u_2} {R : Type u_5} [Zero R] [Zero M] [Zero N] [SMulWithZero R M] [SMulWithZero R N] :
          SMulWithZero R (M × N)
          Equations
            source
            instance Prod.mulActionWithZero {M : Type u_1} {N : Type u_2} {R : Type u_5} [MonoidWithZero R] [Zero M] [Zero N] [MulActionWithZero R M] [MulActionWithZero R N] :
            MulActionWithZero R (M × N)
            Equations

              Scalar multiplication as a homomorphism #

              source
              @[reducible, inline]
              abbrev DistribMulAction.prodOfSMulCommClass (M : Type u_1) (N : Type u_2) (α : Type u_3) [Monoid M] [Monoid N] [AddMonoid α] [DistribMulAction M α] [DistribMulAction N α] [SMulCommClass M N α] :
              DistribMulAction (M × N) α

              Construct a DistribMulAction by a product monoid from DistribMulActions by the factors.

              Equations
                Instances For
                  source
                  def DistribMulAction.prodEquiv (M : Type u_1) (N : Type u_2) (α : Type u_3) [Monoid M] [Monoid N] [AddMonoid α] :
                  DistribMulAction (M × N) α ≃ (x : DistribMulAction M α) ×' (x_1 : DistribMulAction N α) ×' SMulCommClass M N α

                  A DistribMulAction by a product monoid is equivalent to commuting DistribMulActions by the factors.

                  Equations
                    Instances For