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_vadd {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_vadd α (f i)] :
has_vadd α (Π (i : I), f i)
@[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
theorem pi.vadd_def {I : Type u} {f : I → Type v} (x : Π (i : I), f i) {α : Type u_1} [Π (i : I), has_vadd α (f i)] (s : α) :
s +ᵥ x = λ (i : I), s +ᵥ x i
theorem pi.smul_def {I : Type u} {f : I → Type v} (x : Π (i : I), f i) {α : Type u_1} [Π (i : I), has_scalar α (f i)] (s : α) :
s x = λ (i : I), s x i
@[simp]
theorem pi.vadd_apply {I : Type u} {f : I → Type v} (x : Π (i : I), f i) (i : I) {α : Type u_1} [Π (i : I), has_vadd α (f i)] (s : α) :
(s +ᵥ x) 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 : α) :
(s x) i = s x i
@[instance]
def pi.has_vadd' {I : Type u} {f : I → Type v} {g : I → Type u_1} [Π (i : I), has_vadd (f i) (g i)] :
has_vadd (Π (i : I), f i) (Π (i : I), g 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.vadd_apply' {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [Π (i : I), has_vadd (f i) (g i)] (s : Π (i : I), f i) (x : Π (i : I), g i) :
(s +ᵥ x) 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) :
(s x) i = s i x i
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
@[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.vadd_comm_class {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [Π (i : I), has_vadd α (f i)] [Π (i : I), has_vadd β (f i)] [∀ (i : I), vadd_comm_class α β (f i)] :
vadd_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.vadd_comm_class' {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [Π (i : I), has_vadd α (g i)] [Π (i : I), has_vadd (f i) (g i)] [∀ (i : I), vadd_comm_class α (f i) (g i)] :
vadd_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.vadd_comm_class'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [Π (i : I), has_vadd (g i) (h i)] [Π (i : I), has_vadd (f i) (h i)] [∀ (i : I), vadd_comm_class (f i) (g i) (h i)] :
vadd_comm_class (Π (i : I), f i) (Π (i : I), g i) (Π (i : I), h i)
theorem pi.has_faithful_vadd_at {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_vadd α (f i)] [∀ (i : I), nonempty (f i)] (i : I) [has_faithful_vadd α (f i)] :
has_faithful_vadd α (Π (i : I), f i)
theorem pi.has_faithful_scalar_at {I : Type u} {f : I → Type v} {α : Type u_1} [Π (i : I), has_scalar α (f i)] [∀ (i : I), nonempty (f i)] (i : I) [has_faithful_scalar α (f i)] :
has_faithful_scalar α (Π (i : I), f i)

If f i has a faithful scalar action for a given i, then so does Π i, f i. This is not an instance as i cannot be inferred.

@[instance]
def pi.has_faithful_scalar {I : Type u} {f : I → Type v} {α : Type u_1} [nonempty I] [Π (i : I), has_scalar α (f i)] [∀ (i : I), nonempty (f i)] [∀ (i : I), has_faithful_scalar α (f i)] :
has_faithful_scalar α (Π (i : I), f i)
@[instance]
def pi.has_faithful_vadd {I : Type u} {f : I → Type v} {α : Type u_1} [nonempty I] [Π (i : I), has_vadd α (f i)] [∀ (i : I), nonempty (f i)] [∀ (i : I), has_faithful_vadd α (f i)] :
has_faithful_vadd α (Π (i : I), f i)
@[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
@[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
@[instance]
def pi.add_action {I : Type u} {f : I → Type v} (α : Type u_1) {m : add_monoid α} [Π (i : I), add_action α (f i)] :
add_action α (Π (i : I), f 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.add_action' {I : Type u} {f : I → Type v} {g : I → Type u_1} {m : Π (i : I), add_monoid (f i)} [Π (i : I), add_action (f i) (g i)] :
add_action (Π (i : I), f i) (Π (i : I), g i)
@[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.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
@[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
@[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} {α : Type u_1} {β : Type u_2} [monoid α] [add_monoid β] [distrib_mul_action α β] [decidable_eq I] (i : I) (r : α) (x : β) :
pi.single i (r x) = r pi.single i x

A version of pi.single_smul for non-dependent functions. It is useful in cases Lean fails to apply pi.single_smul.

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.mul_distrib_mul_action {I : Type u} {f : I → Type v} (α : Type u_1) {m : monoid α} {n : Π (i : I), monoid (f i)} [Π (i : I), mul_distrib_mul_action α (f i)] :
mul_distrib_mul_action α (Π (i : I), f i)
Equations
@[instance]
def pi.mul_distrib_mul_action' {I : Type u} {f : I → Type v} {g : I → Type u_1} {m : Π (i : I), monoid (f i)} {n : Π (i : I), monoid (g i)} [Π (i : I), mul_distrib_mul_action (f i) (g i)] :
mul_distrib_mul_action (Π (i : I), f i) (Π (i : I), g i)
Equations
@[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
@[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
@[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)
theorem function.extend_smul {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_scalar R γ] (r : R) (f : α → β) (g : α → γ) (e : β → γ) :
function.extend f (r g) (r e) = r function.extend f g e
theorem function.extend_vadd {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [has_vadd R γ] (r : R) (f : α → β) (g : α → γ) (e : β → γ) :