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_3} {N : Type u_4} [Zero R] [Zero M] [Zero N] [SMulWithZero R M] [SMulWithZero R N] :
Equations
instance Prod.mulActionWithZero {R : Type u_1} {M : Type u_3} {N : Type u_4} [MonoidWithZero R] [Zero M] [Zero N] [MulActionWithZero R M] [MulActionWithZero R N] :
Equations
instance Prod.instModule {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
Module R (M × N)
Equations
instance Prod.noZeroSMulDivisors {R : Type u_1} {M : Type u_3} {N : Type u_4} {r : Semiring R} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] :
Equations
  • =