Documentation

Mathlib.Algebra.Module.Prod

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] :
Equations
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] :
Equations
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] :
Equations