Pi instances for multiplicative actions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines instances for mul_action and related structures on Pi types.
See also #
group_theory.group_action.optiongroup_theory.group_action.prodgroup_theory.group_action.sigmagroup_theory.group_action.sum
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
pi.vadd_assoc_class''
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
{h : I → Type u_2}
[Π (i : I), has_vadd (f i) (g i)]
[Π (i : I), has_vadd (g i) (h i)]
[Π (i : I), has_vadd (f i) (h i)]
[∀ (i : I), vadd_assoc_class (f i) (g i) (h i)] :
vadd_assoc_class (Π (i : I), f i) (Π (i : I), g i) (Π (i : I), h i)
@[protected, 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_smul (f i) (g i)]
[Π (i : I), has_smul (g i) (h i)]
[Π (i : I), has_smul (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)
@[protected, instance]
def
pi.smul_comm_class
{I : Type u}
{f : I → Type v}
{α : Type u_1}
{β : Type u_2}
[Π (i : I), has_smul α (f i)]
[Π (i : I), has_smul β (f i)]
[∀ (i : I), smul_comm_class α β (f i)] :
smul_comm_class α β (Π (i : I), f i)
@[protected, 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)
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
pi.is_central_vadd
{I : Type u}
{f : I → Type v}
{α : Type u_1}
[Π (i : I), has_vadd α (f i)]
[Π (i : I), has_vadd αᵃᵒᵖ (f i)]
[∀ (i : I), is_central_vadd α (f i)] :
is_central_vadd α (Π (i : I), f i)
@[protected, instance]
def
pi.is_central_scalar
{I : Type u}
{f : I → Type v}
{α : Type u_1}
[Π (i : I), has_smul α (f i)]
[Π (i : I), has_smul αᵐᵒᵖ (f i)]
[∀ (i : I), is_central_scalar α (f i)] :
is_central_scalar α (Π (i : I), f i)
theorem
pi.has_faithful_smul_at
{I : Type u}
{f : I → Type v}
{α : Type u_1}
[Π (i : I), has_smul α (f i)]
[∀ (i : I), nonempty (f i)]
(i : I)
[has_faithful_smul α (f i)] :
has_faithful_smul α (Π (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.
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)
If f i has a faithful additive action for a given i, then
so does Π i, f i. This is not an instance as i cannot be inferred
@[protected, 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)
@[protected, instance]
def
pi.has_faithful_smul
{I : Type u}
{f : I → Type v}
{α : Type u_1}
[nonempty I]
[Π (i : I), has_smul α (f i)]
[∀ (i : I), nonempty (f i)]
[∀ (i : I), has_faithful_smul α (f i)] :
has_faithful_smul α (Π (i : I), f i)
@[protected, 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)
Equations
- pi.add_action α = {to_has_vadd := {vadd := has_vadd.vadd pi.has_vadd}, zero_vadd := _, add_vadd := _}
@[protected, 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_smul := {smul := has_smul.smul pi.has_smul}, one_smul := _, mul_smul := _}
@[protected, 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)
Equations
- pi.add_action' = {to_has_vadd := {vadd := has_vadd.vadd pi.has_vadd'}, zero_vadd := _, add_vadd := _}
@[protected, 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_smul := {smul := has_smul.smul pi.has_smul'}, one_smul := _, mul_smul := _}
@[protected, instance]
def
pi.smul_zero_class
{I : Type u}
{f : I → Type v}
(α : Type u_1)
{n : Π (i : I), has_zero (f i)}
[Π (i : I), smul_zero_class α (f i)] :
smul_zero_class α (Π (i : I), f i)
Equations
- pi.smul_zero_class α = {to_has_smul := pi.has_smul (λ (i : I), smul_zero_class.to_has_smul), smul_zero := _}
@[protected, instance]
def
pi.smul_zero_class'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
{n : Π (i : I), has_zero (g i)}
[Π (i : I), smul_zero_class (f i) (g i)] :
smul_zero_class (Π (i : I), f i) (Π (i : I), g i)
Equations
- pi.smul_zero_class' = {to_has_smul := pi.has_smul' (λ (i : I), smul_zero_class.to_has_smul), smul_zero := _}
@[protected, instance]
def
pi.distrib_smul
{I : Type u}
{f : I → Type v}
(α : Type u_1)
{n : Π (i : I), add_zero_class (f i)}
[Π (i : I), distrib_smul α (f i)] :
distrib_smul α (Π (i : I), f i)
Equations
- pi.distrib_smul α = {to_smul_zero_class := pi.smul_zero_class α (λ (i : I), distrib_smul.to_smul_zero_class), smul_add := _}
@[protected, instance]
def
pi.distrib_smul'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
{n : Π (i : I), add_zero_class (g i)}
[Π (i : I), distrib_smul (f i) (g i)] :
distrib_smul (Π (i : I), f i) (Π (i : I), g i)
Equations
- pi.distrib_smul' = {to_smul_zero_class := pi.smul_zero_class' (λ (i : I), distrib_smul.to_smul_zero_class), smul_add := _}
@[protected, 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_smul := mul_action.to_has_smul (pi.mul_action α), one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}
@[protected, 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 := {to_has_smul := mul_action.to_has_smul pi.mul_action', one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}
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) :
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 : β) :
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) :
@[protected, 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
- pi.mul_distrib_mul_action α = {to_mul_action := {to_has_smul := mul_action.to_has_smul (pi.mul_action α), one_smul := _, mul_smul := _}, smul_mul := _, smul_one := _}
@[protected, 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
- pi.mul_distrib_mul_action' = {to_mul_action := pi.mul_action' (λ (i : I), mul_distrib_mul_action.to_mul_action), smul_mul := _, smul_one := _}
@[protected, instance]
Non-dependent version of pi.has_vadd. Lean gets confused by the dependent instance
if this is not present.
Equations
@[protected, instance]
Non-dependent version of pi.has_smul. Lean gets confused by the dependent instance if this
is not present.
Equations
@[protected, instance]
def
function.smul_comm_class
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{M : Type u_4}
[has_smul α M]
[has_smul β M]
[smul_comm_class α β M] :
smul_comm_class α β (ι → M)
Non-dependent version of pi.smul_comm_class. Lean gets confused by the dependent instance if
this is not present.
@[protected, instance]
def
function.vadd_comm_class
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{M : Type u_4}
[has_vadd α M]
[has_vadd β M]
[vadd_comm_class α β M] :
vadd_comm_class α β (ι → M)
Non-dependent version of pi.vadd_comm_class. Lean gets confused by the dependent
instance if this is not present.
theorem
function.update_vadd
{I : Type u}
{f : I → Type v}
{α : Type u_1}
[Π (i : I), has_vadd α (f i)]
[decidable_eq I]
(c : α)
(f₁ : Π (i : I), f i)
(i : I)
(x₁ : f i) :
function.update (c +ᵥ f₁) i (c +ᵥ x₁) = c +ᵥ function.update f₁ i x₁
theorem
function.update_smul
{I : Type u}
{f : I → Type v}
{α : Type u_1}
[Π (i : I), has_smul α (f i)]
[decidable_eq I]
(c : α)
(f₁ : Π (i : I), f i)
(i : I)
(x₁ : f i) :
function.update (c • f₁) i (c • x₁) = c • function.update f₁ i x₁