Prod instances for module and multiplicative actions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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] :
smul_with_zero R (M × N)
Equations
- prod.smul_with_zero = {to_smul_zero_class := {to_has_smul := {smul := has_smul.smul prod.has_smul}, smul_zero := _}, zero_smul := _}
@[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] :
mul_action_with_zero R (M × N)
Equations
- prod.mul_action_with_zero = {to_mul_action := {to_has_smul := mul_action.to_has_smul prod.mul_action, one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}
@[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] :
Equations
- prod.module = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action prod.distrib_mul_action, smul_zero := _, smul_add := _}, add_smul := _, zero_smul := _}
@[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] :
no_zero_smul_divisors R (M × N)