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]
:
Equations
- Prod.instModule = { toDistribMulAction := Prod.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }