mathlib documentation

algebra.module.pi

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
@[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 : α) :
(s x) i = s x i
@[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
@[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) :
(s x) i = s i x 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)
@[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)
@[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)
@[instance]
def pi.smul_comm_class {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [Π (i : I), has_scalar α (f i)] [Π (i : I), has_scalar β (f i)] [∀ (i : I), smul_comm_class α β (f i)] :
smul_comm_class α β (Π (i : I), f i)
@[instance]
def pi.smul_comm_class' {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [Π (i : I), has_scalar α (g i)] [Π (i : I), has_scalar (f i) (g i)] [∀ (i : I), smul_comm_class α (f i) (g i)] :
smul_comm_class α (Π (i : I), f i) (Π (i : I), g i)
@[instance]
def pi.smul_comm_class'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [Π (i : I), has_scalar (g i) (h i)] [Π (i : I), has_scalar (f i) (h i)] [∀ (i : I), smul_comm_class (f i) (g i) (h i)] :
smul_comm_class (Π (i : I), f i) (Π (i : I), g i) (Π (i : I), h i)
@[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
@[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
@[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
@[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
theorem pi.single_smul {I : Type u} {f : I → Type v} {α : Type u_1} [monoid α] [Π (i : I), add_monoid (f i)] [Π (i : I), distrib_mul_action α (f i)] [decidable_eq I] (i : I) (r : α) (x : f i) :
pi.single i (r x) = r pi.single i x
theorem pi.single_smul' {I : Type u} {f : I → Type v} {g : I → Type u_1} [Π (i : I), monoid_with_zero (f i)] [Π (i : I), add_monoid (g i)] [Π (i : I), distrib_mul_action (f i) (g i)] [decidable_eq I] (i : I) (r : f i) (x : g i) :
@[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
@[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
@[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), semimodule α (f i)] [∀ (i : I), no_zero_smul_divisors α (f i)] :
no_zero_smul_divisors α (Π (i : I), f i)