Prod instances for module and multiplicative actions
This file defines instances for binary product of modules
@[instance]
def
prod.has_scalar
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α β]
[has_scalar α γ] :
has_scalar α (β × γ)
@[simp]
theorem
prod.smul_fst
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α β]
[has_scalar α γ]
(a : α)
(x : β × γ) :
@[simp]
theorem
prod.smul_snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α β]
[has_scalar α γ]
(a : α)
(x : β × γ) :
@[simp]
theorem
prod.smul_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[has_scalar α β]
[has_scalar α γ]
(a : α)
(b : β)
(c : γ) :
@[instance]
def
prod.semimodule
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{r : semiring α}
[add_comm_monoid β]
[add_comm_monoid γ]
[semimodule α β]
[semimodule α γ] :
semimodule α (β × γ)
Equations
- prod.semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul prod.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}