Prod instances for module and multiplicative actions

This file defines instances for binary product of modules

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 := ⋯ }