mathlib documentation

algebra.module.prod

Prod instances for module and multiplicative actions #

This file defines instances for binary product of modules

@[instance]
def prod.semimodule {R : Type u_1} {M : Type u_3} {N : Type u_4} {r : semiring R} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] :
semimodule R (M × N)
Equations
@[instance]
def prod.no_zero_smul_divisors {R : Type u_1} {M : Type u_3} {N : Type u_4} {r : semiring R} [add_comm_monoid M] [add_comm_monoid N] [semimodule R M] [semimodule R N] [no_zero_smul_divisors R M] [no_zero_smul_divisors R N] :