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}
[inst : Zero R]
[inst : Zero M]
[inst : Zero N]
[inst : SMulWithZero R M]
[inst : 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_2}
{N : Type u_3}
[inst : MonoidWithZero R]
[inst : Zero M]
[inst : Zero N]
[inst : MulActionWithZero R M]
[inst : MulActionWithZero R N]
:
MulActionWithZero R (M × N)
instance
Prod.module
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
:
{x : Semiring R} →
[inst : AddCommMonoid M] →
[inst_1 : AddCommMonoid N] → [inst_2 : Module R M] → [inst_3 : 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_2}
{N : Type u_3}
{r : Semiring R}
[inst : AddCommMonoid M]
[inst : AddCommMonoid N]
[inst : Module R M]
[inst : Module R N]
[inst : NoZeroSMulDivisors R M]
[inst : NoZeroSMulDivisors R N]
:
NoZeroSMulDivisors R (M × N)