mathlib documentation

algebra.module.prod

Prod instances for module and multiplicative actions #

This file defines instances for binary product of modules

@[protected, instance]
def prod.smul_with_zero {R : Type u_1} {M : Type u_3} {N : Type u_4} [has_zero R] [has_zero M] [has_zero N] [smul_with_zero R M] [smul_with_zero R N] :
Equations
@[protected, instance]
def prod.mul_action_with_zero {R : Type u_1} {M : Type u_3} {N : Type u_4} [monoid_with_zero R] [has_zero M] [has_zero N] [mul_action_with_zero R M] [mul_action_with_zero R N] :
Equations
@[protected, instance]
def prod.module {R : Type u_1} {M : Type u_3} {N : Type u_4} {r : semiring R} [add_comm_monoid M] [add_comm_monoid N] [module R M] [module R N] :
module R (M × N)
Equations
@[protected, 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] [module R M] [module R N] [no_zero_smul_divisors R M] [no_zero_smul_divisors R N] :