Pi instances for multiplicative actions

This file defines instances for MulAction and related structures on Pi types.

See also

• Mathlib.Algebra.Group.Action.Option
• Mathlib.Algebra.Group.Action.Prod
• Mathlib.Algebra.Group.Action.Sigma
• Mathlib.Algebra.Group.Action.Sum

instance Pi.vadd' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → VAdd (α i) (β i)] : VAdd ((i : ι) → α i) ((i : ι) → β i)

Equations

• Pi.vadd' = { vadd := fun (s : (i : ι) → α i) (x : (i : ι) → β i) (i : ι) => s i +ᵥ x i }

instance Pi.smul' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → SMul (α i) (β i)] : SMul ((i : ι) → α i) ((i : ι) → β i)

Equations

• Pi.smul' = { smul := fun (s : (i : ι) → α i) (x : (i : ι) → β i) (i : ι) => s i • x i }

theorem Pi.vadd_def' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → VAdd (α i) (β i)] (s : (i : ι) → α i) (x : (i : ι) → β i) : s +ᵥ x = fun (i : ι) => s i +ᵥ x i

theorem Pi.smul_def' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → SMul (α i) (β i)] (s : (i : ι) → α i) (x : (i : ι) → β i) : s • x = fun (i : ι) => s i • x i

@[simp]

theorem Pi.vadd_apply' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} (i : ι) [(i : ι) → VAdd (α i) (β i)] (s : (i : ι) → α i) (x : (i : ι) → β i) : (s +ᵥ x) i = s i +ᵥ x i

@[simp]

theorem Pi.smul_apply' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} (i : ι) [(i : ι) → SMul (α i) (β i)] (s : (i : ι) → α i) (x : (i : ι) → β i) : (s • x) i = s i • x i

instance Pi.vaddAssocClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [VAdd M N] [(i : ι) → VAdd N (α i)] [(i : ι) → VAdd M (α i)] [∀ (i : ι), VAddAssocClass M N (α i)] : VAddAssocClass M N ((i : ι) → α i)

Equations

• ⋯ = ⋯

instance Pi.isScalarTower {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [SMul M N] [(i : ι) → SMul N (α i)] [(i : ι) → SMul M (α i)] [∀ (i : ι), IsScalarTower M N (α i)] : IsScalarTower M N ((i : ι) → α i)

Equations

• ⋯ = ⋯

instance Pi.vaddAssocClass' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → VAdd M (α i)] [(i : ι) → VAdd (α i) (β i)] [(i : ι) → VAdd M (β i)] [∀ (i : ι), VAddAssocClass M (α i) (β i)] : VAddAssocClass M ((i : ι) → α i) ((i : ι) → β i)

Equations

• ⋯ = ⋯

instance Pi.isScalarTower' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → SMul M (α i)] [(i : ι) → SMul (α i) (β i)] [(i : ι) → SMul M (β i)] [∀ (i : ι), IsScalarTower M (α i) (β i)] : IsScalarTower M ((i : ι) → α i) ((i : ι) → β i)

Equations

• ⋯ = ⋯

instance Pi.vaddAssocClass'' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [(i : ι) → VAdd (α i) (β i)] [(i : ι) → VAdd (β i) (γ i)] [(i : ι) → VAdd (α i) (γ i)] [∀ (i : ι), VAddAssocClass (α i) (β i) (γ i)] : VAddAssocClass ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)

Equations

• ⋯ = ⋯

instance Pi.isScalarTower'' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [(i : ι) → SMul (α i) (β i)] [(i : ι) → SMul (β i) (γ i)] [(i : ι) → SMul (α i) (γ i)] [∀ (i : ι), IsScalarTower (α i) (β i) (γ i)] : IsScalarTower ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)

Equations

• ⋯ = ⋯

instance Pi.vaddCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] [(i : ι) → VAdd N (α i)] [∀ (i : ι), VAddCommClass M N (α i)] : VAddCommClass M N ((i : ι) → α i)

Equations

• ⋯ = ⋯

instance Pi.smulCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] [(i : ι) → SMul N (α i)] [∀ (i : ι), SMulCommClass M N (α i)] : SMulCommClass M N ((i : ι) → α i)

Equations

• ⋯ = ⋯

instance Pi.vaddCommClass' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → VAdd M (β i)] [(i : ι) → VAdd (α i) (β i)] [∀ (i : ι), VAddCommClass M (α i) (β i)] : VAddCommClass M ((i : ι) → α i) ((i : ι) → β i)

Equations

• ⋯ = ⋯

instance Pi.smulCommClass' {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → SMul M (β i)] [(i : ι) → SMul (α i) (β i)] [∀ (i : ι), SMulCommClass M (α i) (β i)] : SMulCommClass M ((i : ι) → α i) ((i : ι) → β i)

Equations

• ⋯ = ⋯

instance Pi.vaddCommClass'' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [(i : ι) → VAdd (β i) (γ i)] [(i : ι) → VAdd (α i) (γ i)] [∀ (i : ι), VAddCommClass (α i) (β i) (γ i)] : VAddCommClass ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)

Equations

• ⋯ = ⋯

instance Pi.smulCommClass'' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [(i : ι) → SMul (β i) (γ i)] [(i : ι) → SMul (α i) (γ i)] [∀ (i : ι), SMulCommClass (α i) (β i) (γ i)] : SMulCommClass ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)

Equations

• ⋯ = ⋯

instance Pi.isCentralVAdd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] [(i : ι) → VAdd Mᵃᵒᵖ (α i)] [∀ (i : ι), IsCentralVAdd M (α i)] : IsCentralVAdd M ((i : ι) → α i)

Equations

• ⋯ = ⋯

instance Pi.isCentralScalar {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] [(i : ι) → SMul Mᵐᵒᵖ (α i)] [∀ (i : ι), IsCentralScalar M (α i)] : IsCentralScalar M ((i : ι) → α i)

Equations

• ⋯ = ⋯

theorem Pi.faithfulVAdd_at {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] [∀ (i : ι), Nonempty (α i)] (i : ι) [FaithfulVAdd M (α i)] : FaithfulVAdd M ((i : ι) → α i)

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

theorem Pi.faithfulSMul_at {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] [∀ (i : ι), Nonempty (α i)] (i : ι) [FaithfulSMul M (α i)] : FaithfulSMul M ((i : ι) → α i)

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

instance Pi.faithfulVAdd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Nonempty ι] [(i : ι) → VAdd M (α i)] [∀ (i : ι), Nonempty (α i)] [∀ (i : ι), FaithfulVAdd M (α i)] : FaithfulVAdd M ((i : ι) → α i)

Equations

• ⋯ = ⋯

instance Pi.faithfulSMul {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Nonempty ι] [(i : ι) → SMul M (α i)] [∀ (i : ι), Nonempty (α i)] [∀ (i : ι), FaithfulSMul M (α i)] : FaithfulSMul M ((i : ι) → α i)

Equations

• ⋯ = ⋯

instance Pi.addAction {ι : Type u_1} {α : ι → Type u_4} (M : Type u_7) {m : AddMonoid M} [(i : ι) → AddAction M (α i)] : AddAction M ((i : ι) → α i)

Equations

• Pi.addAction M = AddAction.mk ⋯ ⋯

theorem Pi.addAction.proof_1 {ι : Type u_1} {α : ι → Type u_2} (M : Type u_3) {m : AddMonoid M} [(i : ι) → AddAction M (α i)] : ∀ (x : (i : ι) → α i), 0 +ᵥ x = x

theorem Pi.addAction.proof_2 {ι : Type u_1} {α : ι → Type u_2} (M : Type u_3) {m : AddMonoid M} [(i : ι) → AddAction M (α i)] : ∀ (x x_1 : M) (x_2 : (i : ι) → α i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)

instance Pi.mulAction {ι : Type u_1} {α : ι → Type u_4} (M : Type u_7) {m : Monoid M} [(i : ι) → MulAction M (α i)] : MulAction M ((i : ι) → α i)

Equations

• Pi.mulAction M = MulAction.mk ⋯ ⋯

theorem Pi.addAction'.proof_2 {ι : Type u_1} {α : ι → Type u_3} {β : ι → Type u_2} {m : (i : ι) → AddMonoid (α i)} [(i : ι) → AddAction (α i) (β i)] : ∀ (x x_1 : (i : ι) → α i) (x_2 : (i : ι) → β i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)

theorem Pi.addAction'.proof_1 {ι : Type u_1} {α : ι → Type u_3} {β : ι → Type u_2} {m : (i : ι) → AddMonoid (α i)} [(i : ι) → AddAction (α i) (β i)] : ∀ (x : (i : ι) → β i), 0 +ᵥ x = x

instance Pi.addAction' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {m : (i : ι) → AddMonoid (α i)} [(i : ι) → AddAction (α i) (β i)] : AddAction ((i : ι) → α i) ((i : ι) → β i)

Equations

• Pi.addAction' = AddAction.mk ⋯ ⋯

instance Pi.mulAction' {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {m : (i : ι) → Monoid (α i)} [(i : ι) → MulAction (α i) (β i)] : MulAction ((i : ι) → α i) ((i : ι) → β i)

Equations

• Pi.mulAction' = MulAction.mk ⋯ ⋯

instance Function.hasVAdd {ι : Type u_1} {M : Type u_2} {α : Type u_7} [VAdd M α] : VAdd M (ι → α)

Non-dependent version of Pi.vadd. Lean gets confused by the dependent instance if this is not present.

Equations

• Function.hasVAdd = Pi.instVAdd

instance Function.hasSMul {ι : Type u_1} {M : Type u_2} {α : Type u_7} [SMul M α] : SMul M (ι → α)

Non-dependent version of Pi.smul. Lean gets confused by the dependent instance if this is not present.

Equations

• Function.hasSMul = Pi.instSMul

instance Function.vaddCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : Type u_7} [VAdd M α] [VAdd N α] [VAddCommClass M N α] : VAddCommClass M N (ι → α)

Non-dependent version of Pi.vaddCommClass. Lean gets confused by the dependent instance if this is not present.

Equations

• ⋯ = ⋯

instance Function.smulCommClass {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : Type u_7} [SMul M α] [SMul N α] [SMulCommClass M N α] : SMulCommClass M N (ι → α)

Non-dependent version of Pi.smulCommClass. Lean gets confused by the dependent instance if this is not present.

Equations

• ⋯ = ⋯

theorem Function.update_vadd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] [DecidableEq ι] (c : M) (f₁ : (i : ι) → α i) (i : ι) (x₁ : α i) : Function.update (c +ᵥ f₁) i (c +ᵥ x₁) = c +ᵥ Function.update f₁ i x₁

theorem Function.update_smul {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] [DecidableEq ι] (c : M) (f₁ : (i : ι) → α i) (i : ι) (x₁ : α i) : Function.update (c • f₁) i (c • x₁) = c • Function.update f₁ i x₁

theorem Function.extend_vadd {ι : Type u_1} {M : Type u_7} {α : Type u_8} {β : Type u_9} [VAdd M β] (r : M) (f : ι → α) (g : ι → β) (e : α → β) : Function.extend f (r +ᵥ g) (r +ᵥ e) = r +ᵥ Function.extend f g e

theorem Function.extend_smul {ι : Type u_1} {M : Type u_7} {α : Type u_8} {β : Type u_9} [SMul M β] (r : M) (f : ι → α) (g : ι → β) (e : α → β) : Function.extend f (r • g) (r • e) = r • Function.extend f g e

theorem Set.piecewise_vadd {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → VAdd M (α i)] (s : Set ι) [(i : ι) → Decidable (i ∈ s)] (c : M) (f₁ : (i : ι) → α i) (g₁ : (i : ι) → α i) : s.piecewise (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ s.piecewise f₁ g₁

theorem Set.piecewise_smul {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [(i : ι) → SMul M (α i)] (s : Set ι) [(i : ι) → Decidable (i ∈ s)] (c : M) (f₁ : (i : ι) → α i) (g₁ : (i : ι) → α i) : s.piecewise (c • f₁) (c • g₁) = c • s.piecewise f₁ g₁