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_smul α (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_smul := {smul := has_smul.smul pi.has_smul}, 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_smul := {smul := has_smul.smul pi.has_smul'}, 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_smul := mul_action.to_has_smul (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_smul := mul_action.to_has_smul 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
function.module
(I : Type u)
(α : Type u_1)
(β : Type u_2)
[semiring α]
[add_comm_monoid β]
[module α β] :
module α (I → β)
A special case of pi.module for non-dependent types. Lean struggles to elaborate
definitions elsewhere in the library without this.
Equations
- function.module I α β = pi.module I (λ (ᾰ : I), β) α
@[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)