Prod instances for module and multiplicative actions

This file defines instances for binary product of modules

instance Prod.smulWithZero {R : Type u_1} {M : Type u_2} {N : Type u_3} [Zero R] [Zero M] [Zero N] [SMulWithZero R M] [SMulWithZero R N] : SMulWithZero R (M × N)

Equations

• Prod.smulWithZero = { toSMul := Prod.instSMul, smul_zero := ⋯, zero_smul := ⋯ }

instance Prod.mulActionWithZero {R : Type u_1} {M : Type u_2} {N : Type u_3} [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 := ⋯ }

instance Prod.instModule {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : Module R (M × N)

Equations

• Prod.instModule = { toDistribMulAction := Prod.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }