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_reducible]

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 = { toSMul := Prod.instSMul, smul_zero := ⋯ }

@[instance_reducible]

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 = { toSMulZeroClass := Prod.smulZeroClass, smul_add := ⋯ }

@[instance_reducible]

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 = { toMulAction := Prod.mulAction, smul_zero := ⋯, smul_add := ⋯ }

@[instance_reducible]

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 = { toMulAction := Prod.mulAction, smul_one := ⋯, smul_mul := ⋯ }

@[instance_reducible]

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

• Prod.smulWithZero = { toSMulZeroClass := Prod.smulZeroClass, zero_smul := ⋯ }

@[instance_reducible]

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

• Prod.mulActionWithZero = { toMulAction := Prod.mulAction, smul_zero := ⋯, zero_smul := ⋯ }

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 α = { toMulAction := MulAction.prodOfSMulCommClass M N α, smul_zero := ⋯, smul_add := ⋯ }

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.