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 = SMulWithZero.mk ⋯
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 = MulActionWithZero.mk ⋯ ⋯
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]
: