Pi instances for modules #
This file defines instances for module and related structures on Pi Types
theorem
is_smul_regular.pi
{I : Type u}
{f : I → Type v}
{α : Type u_1}
[Π (i : I), has_scalar α (f i)]
{k : α}
(hk : ∀ (i : I), is_smul_regular (f i) k) :
is_smul_regular (Π (i : I), f i) k
@[protected, instance]
def
pi.smul_with_zero
{I : Type u}
{f : I → Type v}
(α : Type u_1)
[has_zero α]
[Π (i : I), has_zero (f i)]
[Π (i : I), smul_with_zero α (f i)] :
smul_with_zero α (Π (i : I), f i)
Equations
- pi.smul_with_zero α = {to_has_scalar := {smul := has_scalar.smul pi.has_scalar}, smul_zero := _, zero_smul := _}
@[protected, instance]
def
pi.smul_with_zero'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
[Π (i : I), has_zero (g i)]
[Π (i : I), has_zero (f i)]
[Π (i : I), smul_with_zero (g i) (f i)] :
smul_with_zero (Π (i : I), g i) (Π (i : I), f i)
Equations
- pi.smul_with_zero' = {to_has_scalar := {smul := has_scalar.smul pi.has_scalar'}, smul_zero := _, zero_smul := _}
@[protected, instance]
def
pi.mul_action_with_zero
{I : Type u}
{f : I → Type v}
(α : Type u_1)
[monoid_with_zero α]
[Π (i : I), has_zero (f i)]
[Π (i : I), mul_action_with_zero α (f i)] :
mul_action_with_zero α (Π (i : I), f i)
Equations
- pi.mul_action_with_zero α = {to_mul_action := {to_has_scalar := mul_action.to_has_scalar (pi.mul_action α), one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}
@[protected, instance]
def
pi.mul_action_with_zero'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
[Π (i : I), monoid_with_zero (g i)]
[Π (i : I), has_zero (f i)]
[Π (i : I), mul_action_with_zero (g i) (f i)] :
mul_action_with_zero (Π (i : I), g i) (Π (i : I), f i)
Equations
- pi.mul_action_with_zero' = {to_mul_action := {to_has_scalar := mul_action.to_has_scalar pi.mul_action', one_smul := _, mul_smul := _}, smul_zero := _, zero_smul := _}
@[protected, instance]
def
pi.module
(I : Type u)
(f : I → Type v)
(α : Type u_1)
{r : semiring α}
{m : Π (i : I), add_comm_monoid (f i)}
[Π (i : I), module α (f i)] :
module α (Π (i : I), f i)
Equations
- pi.module 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 := _}
@[protected, instance]
def
pi.module'
{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), module (f i) (g i)] :
module (Π (i : I), f i) (Π (i : I), g i)
Equations
- pi.module' = {to_distrib_mul_action := pi.distrib_mul_action' (λ (i : I), module.to_distrib_mul_action), add_smul := _, zero_smul := _}
@[protected, instance]
def
pi.no_zero_smul_divisors
{I : Type u}
{f : I → Type v}
(α : Type u_1)
{r : semiring α}
{m : Π (i : I), add_comm_monoid (f i)}
[Π (i : I), module α (f i)]
[∀ (i : I), no_zero_smul_divisors α (f i)] :
no_zero_smul_divisors α (Π (i : I), f i)