Pi instances for module and multiplicative actions
This file defines instances for module, mul_action and related structures on Pi Types
@[instance]
def
pi.has_scalar
{I : Type u}
{f : I → Type v}
{α : Type u_1}
[Π (i : I), has_scalar α (f i)] :
has_scalar α (Π (i : I), f i)
Equations
- pi.has_scalar = {smul := λ (s : α) (x : Π (i : I), f i) (i : I), s • x i}
@[simp]
theorem
pi.smul_apply
{I : Type u}
{f : I → Type v}
(x : Π (i : I), f i)
(i : I)
{α : Type u_1}
[Π (i : I), has_scalar α (f i)]
(s : α) :
@[instance]
def
pi.has_scalar'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
[Π (i : I), has_scalar (f i) (g i)] :
has_scalar (Π (i : I), f i) (Π (i : I), g i)
Equations
- pi.has_scalar' = {smul := λ (s : Π (i : I), f i) (x : Π (i : I), g i) (i : I), s i • x i}
@[simp]
theorem
pi.smul_apply'
{I : Type u}
{f : I → Type v}
(i : I)
{g : I → Type u_1}
[Π (i : I), has_scalar (f i) (g i)]
(s : Π (i : I), f i)
(x : Π (i : I), g i) :
@[instance]
def
pi.is_scalar_tower
{I : Type u}
{f : I → Type v}
{α : Type u_1}
{β : Type u_2}
[has_scalar α β]
[Π (i : I), has_scalar β (f i)]
[Π (i : I), has_scalar α (f i)]
[∀ (i : I), is_scalar_tower α β (f i)] :
is_scalar_tower α β (Π (i : I), f i)
Equations
@[instance]
def
pi.is_scalar_tower'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
{α : Type u_2}
[Π (i : I), has_scalar α (f i)]
[Π (i : I), has_scalar (f i) (g i)]
[Π (i : I), has_scalar α (g i)]
[∀ (i : I), is_scalar_tower α (f i) (g i)] :
is_scalar_tower α (Π (i : I), f i) (Π (i : I), g i)
Equations
@[instance]
def
pi.is_scalar_tower''
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
{h : I → Type u_2}
[Π (i : I), has_scalar (f i) (g i)]
[Π (i : I), has_scalar (g i) (h i)]
[Π (i : I), has_scalar (f i) (h i)]
[∀ (i : I), is_scalar_tower (f i) (g i) (h i)] :
is_scalar_tower (Π (i : I), f i) (Π (i : I), g i) (Π (i : I), h i)
Equations
@[instance]
def
pi.mul_action
{I : Type u}
{f : I → Type v}
(α : Type u_1)
{m : monoid α}
[Π (i : I), mul_action α (f i)] :
mul_action α (Π (i : I), f i)
Equations
- pi.mul_action α = {to_has_scalar := {smul := has_scalar.smul pi.has_scalar}, one_smul := _, mul_smul := _}
@[instance]
def
pi.mul_action'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
{m : Π (i : I), monoid (f i)}
[Π (i : I), mul_action (f i) (g i)] :
mul_action (Π (i : I), f i) (Π (i : I), g i)
Equations
- pi.mul_action' = {to_has_scalar := {smul := has_scalar.smul pi.has_scalar'}, one_smul := _, mul_smul := _}
@[instance]
def
pi.distrib_mul_action
{I : Type u}
{f : I → Type v}
(α : Type u_1)
{m : monoid α}
{n : Π (i : I), add_monoid (f i)}
[Π (i : I), distrib_mul_action α (f i)] :
distrib_mul_action α (Π (i : I), f i)
Equations
- pi.distrib_mul_action α = {to_mul_action := {to_has_scalar := mul_action.to_has_scalar (pi.mul_action α), one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
@[instance]
def
pi.distrib_mul_action'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
{m : Π (i : I), monoid (f i)}
{n : Π (i : I), add_monoid (g i)}
[Π (i : I), distrib_mul_action (f i) (g i)] :
distrib_mul_action (Π (i : I), f i) (Π (i : I), g i)
Equations
- pi.distrib_mul_action' = {to_mul_action := pi.mul_action' (λ (i : I), distrib_mul_action.to_mul_action), smul_add := _, smul_zero := _}
@[instance]
def
pi.semimodule
(I : Type u)
(f : I → Type v)
(α : Type u_1)
{r : semiring α}
{m : Π (i : I), add_comm_monoid (f i)}
[Π (i : I), semimodule α (f i)] :
semimodule α (Π (i : I), f i)
Equations
- pi.semimodule I f α = {to_distrib_mul_action := {to_mul_action := distrib_mul_action.to_mul_action (pi.distrib_mul_action α), smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[instance]
def
pi.semimodule'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
{r : Π (i : I), semiring (f i)}
{m : Π (i : I), add_comm_monoid (g i)}
[Π (i : I), semimodule (f i) (g i)] :
semimodule (Π (i : I), f i) (Π (i : I), g i)
Equations
- pi.semimodule' = {to_distrib_mul_action := pi.distrib_mul_action' (λ (i : I), semimodule.to_distrib_mul_action), add_smul := _, zero_smul := _}