Prod instances for multiplicative actions with zero

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

See also

• Algebra.GroupWithZero.Action.Opposite
• Algebra.GroupWithZero.Action.Pi
• Algebra.GroupWithZero.Action.Units

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)

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)

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

• Prod.smulZeroClass = SMulZeroClass.mk ⋯

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

• Prod.distribSMul = DistribSMul.mk ⋯

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

• Prod.distribMulAction = DistribMulAction.mk ⋯ ⋯

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

• Prod.mulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯

Scalar multiplication as a homomorphism

@[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

• DistribMulAction.prodOfSMulCommClass M N α = DistribMulAction.mk ⋯ ⋯

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

• One or more equations did not get rendered due to their size.