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_3} {N : Type u_4} [Zero R] [Zero M] [Zero N] [SMulWithZero R M] [SMulWithZero R N] : SMulWithZero R (M × N)

Equations

• Prod.smulWithZero = let __src := Prod.smul; SMulWithZero.mk ⋯

instance Prod.mulActionWithZero {R : Type u_1} {M : Type u_3} {N : Type u_4} [MonoidWithZero R] [Zero M] [Zero N] [MulActionWithZero R M] [MulActionWithZero R N] : MulActionWithZero R (M × N)

Equations

• Prod.mulActionWithZero = let __src := Prod.mulAction; MulActionWithZero.mk ⋯ ⋯

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

Equations

• Prod.instModule = let __src := Prod.distribMulAction; Module.mk ⋯ ⋯

instance Prod.noZeroSMulDivisors {R : Type u_1} {M : Type u_3} {N : Type u_4} {r : Semiring R} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] : NoZeroSMulDivisors R (M × N)

Equations

• ⋯ = ⋯