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 (_ : ∀ (x : M × N), 0 • x = 0)

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 (_ : ∀ (x : R), x • 0 = 0) (_ : ∀ (x : M × N), 0 • x = 0)

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

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

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

• @Prod.noZeroSMulDivisors = @Prod.noZeroSMulDivisors.proof_1