Pi instances for multiplicative actions #

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

See also #

GroupTheory.GroupAction.option
GroupTheory.GroupAction.prod
GroupTheory.GroupAction.sigma
GroupTheory.GroupAction.sum

source

instance Pi.vadd' {I : Type u} {f : I → Type v} {g : I → Type u_1} [(i : I) → VAdd (f i) (g i)] :

VAdd ((i : I) → f i) ((i : I) → g i)

Equations

Pi.vadd' = { vadd := fun s x i => s i +ᵥ x i }

source

instance Pi.smul' {I : Type u} {f : I → Type v} {g : I → Type u_1} [(i : I) → SMul (f i) (g i)] :

SMul ((i : I) → f i) ((i : I) → g i)

Equations

Pi.smul' = { smul := fun s x i => s i • x i }

source

@[simp]

theorem Pi.vadd_apply' {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [(i : I) → VAdd (f i) (g i)] (s : (i : I) → f i) (x : (i : I) → g i) :

(((i : I) → f i) +ᵥ ((i : I) → g i)) ((i : I) → g i) instHVAdd s x i = s i +ᵥ x i

source

@[simp]

theorem Pi.smul_apply' {I : Type u} {f : I → Type v} (i : I) {g : I → Type u_1} [(i : I) → SMul (f i) (g i)] (s : (i : I) → f i) (x : (i : I) → g i) :

(((i : I) → f i) • ((i : I) → g i)) ((i : I) → g i) instHSMul s x i = s i • x i

source

instance Pi.vaddAssocClass {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [VAdd α β] [(i : I) → VAdd β (f i)] [(i : I) → VAdd α (f i)] [∀ (i : I), VAddAssocClass α β (f i)] :

VAddAssocClass α β ((i : I) → f i)

Equations

@Pi.vaddAssocClass = @Pi.vaddAssocClass.proof_1

source

theorem Pi.vaddAssocClass.proof_1 {I : Type u_1} {f : I → Type u_2} {α : Type u_3} {β : Type u_4} [VAdd α β] [(i : I) → VAdd β (f i)] [(i : I) → VAdd α (f i)] [∀ (i : I), VAddAssocClass α β (f i)] :

VAddAssocClass α β ((i : I) → f i)

source

instance Pi.isScalarTower {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [SMul α β] [(i : I) → SMul β (f i)] [(i : I) → SMul α (f i)] [∀ (i : I), IsScalarTower α β (f i)] :

IsScalarTower α β ((i : I) → f i)

Equations

@Pi.isScalarTower = @Pi.isScalarTower.proof_1

source

theorem Pi.vaddAssocClass'.proof_1 {I : Type u_1} {f : I → Type u_2} {g : I → Type u_3} {α : Type u_4} [(i : I) → VAdd α (f i)] [(i : I) → VAdd (f i) (g i)] [(i : I) → VAdd α (g i)] [∀ (i : I), VAddAssocClass α (f i) (g i)] :

VAddAssocClass α ((i : I) → f i) ((i : I) → g i)

source

instance Pi.vaddAssocClass' {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [(i : I) → VAdd α (f i)] [(i : I) → VAdd (f i) (g i)] [(i : I) → VAdd α (g i)] [∀ (i : I), VAddAssocClass α (f i) (g i)] :

VAddAssocClass α ((i : I) → f i) ((i : I) → g i)

Equations

@Pi.vaddAssocClass' = @Pi.vaddAssocClass'.proof_1

source

instance Pi.isScalarTower' {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [(i : I) → SMul α (f i)] [(i : I) → SMul (f i) (g i)] [(i : I) → SMul α (g i)] [∀ (i : I), IsScalarTower α (f i) (g i)] :

IsScalarTower α ((i : I) → f i) ((i : I) → g i)

Equations

@Pi.isScalarTower' = @Pi.isScalarTower'.proof_1

source

instance Pi.vaddAssocClass'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [(i : I) → VAdd (f i) (g i)] [(i : I) → VAdd (g i) (h i)] [(i : I) → VAdd (f i) (h i)] [∀ (i : I), VAddAssocClass (f i) (g i) (h i)] :

VAddAssocClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)

Equations

@Pi.vaddAssocClass'' = @Pi.vaddAssocClass''.proof_1

source

theorem Pi.vaddAssocClass''.proof_1 {I : Type u_1} {f : I → Type u_2} {g : I → Type u_3} {h : I → Type u_4} [(i : I) → VAdd (f i) (g i)] [(i : I) → VAdd (g i) (h i)] [(i : I) → VAdd (f i) (h i)] [∀ (i : I), VAddAssocClass (f i) (g i) (h i)] :

VAddAssocClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)

source

instance Pi.isScalarTower'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [(i : I) → SMul (f i) (g i)] [(i : I) → SMul (g i) (h i)] [(i : I) → SMul (f i) (h i)] [∀ (i : I), IsScalarTower (f i) (g i) (h i)] :

IsScalarTower ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)

Equations

@Pi.isScalarTower'' = @Pi.isScalarTower''.proof_1

source

theorem Pi.vaddCommClass.proof_1 {I : Type u_1} {f : I → Type u_2} {α : Type u_3} {β : Type u_4} [(i : I) → VAdd α (f i)] [(i : I) → VAdd β (f i)] [∀ (i : I), VAddCommClass α β (f i)] :

VAddCommClass α β ((i : I) → f i)

source

instance Pi.vaddCommClass {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [(i : I) → VAdd α (f i)] [(i : I) → VAdd β (f i)] [∀ (i : I), VAddCommClass α β (f i)] :

VAddCommClass α β ((i : I) → f i)

Equations

@Pi.vaddCommClass = @Pi.vaddCommClass.proof_1

source

instance Pi.smulCommClass {I : Type u} {f : I → Type v} {α : Type u_1} {β : Type u_2} [(i : I) → SMul α (f i)] [(i : I) → SMul β (f i)] [∀ (i : I), SMulCommClass α β (f i)] :

SMulCommClass α β ((i : I) → f i)

Equations

@Pi.smulCommClass = @Pi.smulCommClass.proof_1

source

theorem Pi.vaddCommClass'.proof_1 {I : Type u_1} {f : I → Type u_2} {g : I → Type u_3} {α : Type u_4} [(i : I) → VAdd α (g i)] [(i : I) → VAdd (f i) (g i)] [∀ (i : I), VAddCommClass α (f i) (g i)] :

VAddCommClass α ((i : I) → f i) ((i : I) → g i)

source

instance Pi.vaddCommClass' {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [(i : I) → VAdd α (g i)] [(i : I) → VAdd (f i) (g i)] [∀ (i : I), VAddCommClass α (f i) (g i)] :

VAddCommClass α ((i : I) → f i) ((i : I) → g i)

Equations

@Pi.vaddCommClass' = @Pi.vaddCommClass'.proof_1

source

instance Pi.smulCommClass' {I : Type u} {f : I → Type v} {g : I → Type u_1} {α : Type u_2} [(i : I) → SMul α (g i)] [(i : I) → SMul (f i) (g i)] [∀ (i : I), SMulCommClass α (f i) (g i)] :

SMulCommClass α ((i : I) → f i) ((i : I) → g i)

Equations

@Pi.smulCommClass' = @Pi.smulCommClass'.proof_1

source

instance Pi.vaddCommClass'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [(i : I) → VAdd (g i) (h i)] [(i : I) → VAdd (f i) (h i)] [∀ (i : I), VAddCommClass (f i) (g i) (h i)] :

VAddCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)

Equations

@Pi.vaddCommClass'' = @Pi.vaddCommClass''.proof_1

source

theorem Pi.vaddCommClass''.proof_1 {I : Type u_1} {f : I → Type u_2} {g : I → Type u_3} {h : I → Type u_4} [(i : I) → VAdd (g i) (h i)] [(i : I) → VAdd (f i) (h i)] [∀ (i : I), VAddCommClass (f i) (g i) (h i)] :

VAddCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)

source

instance Pi.smulCommClass'' {I : Type u} {f : I → Type v} {g : I → Type u_1} {h : I → Type u_2} [(i : I) → SMul (g i) (h i)] [(i : I) → SMul (f i) (h i)] [∀ (i : I), SMulCommClass (f i) (g i) (h i)] :

SMulCommClass ((i : I) → f i) ((i : I) → g i) ((i : I) → h i)

Equations

@Pi.smulCommClass'' = @Pi.smulCommClass''.proof_1

source

instance Pi.isCentralVAdd {I : Type u} {f : I → Type v} {α : Type u_1} [(i : I) → VAdd α (f i)] [(i : I) → VAdd αᵃᵒᵖ (f i)] [∀ (i : I), IsCentralVAdd α (f i)] :

IsCentralVAdd α ((i : I) → f i)

Equations

@Pi.isCentralVAdd = @Pi.isCentralVAdd.proof_1

source

theorem Pi.isCentralVAdd.proof_1 {I : Type u_1} {f : I → Type u_2} {α : Type u_3} [(i : I) → VAdd α (f i)] [(i : I) → VAdd αᵃᵒᵖ (f i)] [∀ (i : I), IsCentralVAdd α (f i)] :

IsCentralVAdd α ((i : I) → f i)

source

instance Pi.isCentralScalar {I : Type u} {f : I → Type v} {α : Type u_1} [(i : I) → SMul α (f i)] [(i : I) → SMul αᵐᵒᵖ (f i)] [∀ (i : I), IsCentralScalar α (f i)] :

IsCentralScalar α ((i : I) → f i)

Equations

@Pi.isCentralScalar = @Pi.isCentralScalar.proof_1

source

theorem Pi.faithfulVAdd_at {I : Type u} {f : I → Type v} {α : Type u_1} [(i : I) → VAdd α (f i)] [∀ (i : I), Nonempty (f i)] (i : I) [FaithfulVAdd α (f i)] :

FaithfulVAdd α ((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

source

theorem Pi.faithfulSMul_at {I : Type u} {f : I → Type v} {α : Type u_1} [(i : I) → SMul α (f i)] [∀ (i : I), Nonempty (f i)] (i : I) [FaithfulSMul α (f i)] :

FaithfulSMul α ((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.

source

instance Pi.faithfulVAdd {I : Type u} {f : I → Type v} {α : Type u_1} [Nonempty I] [(i : I) → VAdd α (f i)] [∀ (i : I), Nonempty (f i)] [∀ (i : I), FaithfulVAdd α (f i)] :

FaithfulVAdd α ((i : I) → f i)

Equations

@Pi.faithfulVAdd = @Pi.faithfulVAdd.proof_1

source

theorem Pi.faithfulVAdd.proof_1 {I : Type u_1} {f : I → Type u_2} {α : Type u_3} [Nonempty I] [(i : I) → VAdd α (f i)] [∀ (i : I), Nonempty (f i)] [∀ (i : I), FaithfulVAdd α (f i)] :

FaithfulVAdd α ((i : I) → f i)

source

abbrev Pi.faithfulVAdd.match_1 {I : Type u_1} (motive : Nonempty I → Prop) :

(x : Nonempty I) → ((i : I) → motive (_ : Nonempty I)) → motive x

Equations

Pi.faithfulVAdd.match_1 motive x h_1 = Nonempty.casesOn x fun val => h_1 val

Instances For

source

instance Pi.faithfulSMul {I : Type u} {f : I → Type v} {α : Type u_1} [Nonempty I] [(i : I) → SMul α (f i)] [∀ (i : I), Nonempty (f i)] [∀ (i : I), FaithfulSMul α (f i)] :

FaithfulSMul α ((i : I) → f i)

Equations

@Pi.faithfulSMul = @Pi.faithfulSMul.proof_1

source

theorem Pi.addAction.proof_2 {I : Type u_1} {f : I → Type u_2} (α : Type u_3) {m : AddMonoid α} [(i : I) → AddAction α (f i)] :

∀ (x x_1 : α) (x_2 : (i : I) → f i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)

source

instance Pi.addAction {I : Type u} {f : I → Type v} (α : Type u_1) {m : AddMonoid α} [(i : I) → AddAction α (f i)] :

AddAction α ((i : I) → f i)

Equations

Pi.addAction α = AddAction.mk (_ : ∀ (x : (i : I) → f i), 0 +ᵥ x = x) (_ : ∀ (x x_1 : α) (x_2 : (i : I) → f i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2))

source

theorem Pi.addAction.proof_1 {I : Type u_1} {f : I → Type u_2} (α : Type u_3) {m : AddMonoid α} [(i : I) → AddAction α (f i)] :

∀ (x : (i : I) → f i), 0 +ᵥ x = x

source

instance Pi.mulAction {I : Type u} {f : I → Type v} (α : Type u_1) {m : Monoid α} [(i : I) → MulAction α (f i)] :

MulAction α ((i : I) → f i)

Equations

Pi.mulAction α = MulAction.mk (_ : ∀ (x : (i : I) → f i), 1 • x = x) (_ : ∀ (x x_1 : α) (x_2 : (i : I) → f i), (x * x_1) • x_2 = x • x_1 • x_2)

source

theorem Pi.addAction'.proof_2 {I : Type u_1} {f : I → Type u_3} {g : I → Type u_2} {m : (i : I) → AddMonoid (f i)} [(i : I) → AddAction (f i) (g i)] :

∀ (x x_1 : (i : I) → f i) (x_2 : (i : I) → g i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2)

source

instance Pi.addAction' {I : Type u} {f : I → Type v} {g : I → Type u_1} {m : (i : I) → AddMonoid (f i)} [(i : I) → AddAction (f i) (g i)] :

AddAction ((i : I) → f i) ((i : I) → g i)

Equations

Pi.addAction' = AddAction.mk (_ : ∀ (x : (i : I) → g i), 0 +ᵥ x = x) (_ : ∀ (x x_1 : (i : I) → f i) (x_2 : (i : I) → g i), x + x_1 +ᵥ x_2 = x +ᵥ (x_1 +ᵥ x_2))

source

theorem Pi.addAction'.proof_1 {I : Type u_1} {f : I → Type u_3} {g : I → Type u_2} {m : (i : I) → AddMonoid (f i)} [(i : I) → AddAction (f i) (g i)] :

∀ (x : (i : I) → g i), 0 +ᵥ x = x

source

instance Pi.mulAction' {I : Type u} {f : I → Type v} {g : I → Type u_1} {m : (i : I) → Monoid (f i)} [(i : I) → MulAction (f i) (g i)] :

MulAction ((i : I) → f i) ((i : I) → g i)

Equations

Pi.mulAction' = MulAction.mk (_ : ∀ (x : (i : I) → g i), 1 • x = x) (_ : ∀ (x x_1 : (i : I) → f i) (x_2 : (i : I) → g i), (x * x_1) • x_2 = x • x_1 • x_2)

source

instance Pi.smulZeroClass {I : Type u} {f : I → Type v} (α : Type u_1) {n : (i : I) → Zero (f i)} [(i : I) → SMulZeroClass α (f i)] :

SMulZeroClass α ((i : I) → f i)

Equations

Pi.smulZeroClass α = SMulZeroClass.mk (_ : ∀ (x : α), x • 0 = 0)

source

instance Pi.smulZeroClass' {I : Type u} {f : I → Type v} {g : I → Type u_1} {n : (i : I) → Zero (g i)} [(i : I) → SMulZeroClass (f i) (g i)] :

SMulZeroClass ((i : I) → f i) ((i : I) → g i)

Equations

Pi.smulZeroClass' = SMulZeroClass.mk (_ : ∀ (a : (i : I) → f i), a • 0 = 0)

source

instance Pi.distribSMul {I : Type u} {f : I → Type v} (α : Type u_1) {n : (i : I) → AddZeroClass (f i)} [(i : I) → DistribSMul α (f i)] :

DistribSMul α ((i : I) → f i)

Equations

Pi.distribSMul α = DistribSMul.mk (_ : ∀ (x : α) (x_1 x_2 : (i : I) → f i), x • (x_1 + x_2) = x • x_1 + x • x_2)

source

instance Pi.distribSMul' {I : Type u} {f : I → Type v} {g : I → Type u_1} {n : (i : I) → AddZeroClass (g i)} [(i : I) → DistribSMul (f i) (g i)] :

DistribSMul ((i : I) → f i) ((i : I) → g i)

Equations

Pi.distribSMul' = DistribSMul.mk (_ : ∀ (a : (i : I) → f i) (x y : (i : I) → g i), a • (x + y) = a • x + a • y)

source

instance Pi.distribMulAction {I : Type u} {f : I → Type v} (α : Type u_1) {m : Monoid α} {n : (i : I) → AddMonoid (f i)} [(i : I) → DistribMulAction α (f i)] :

DistribMulAction α ((i : I) → f i)

Equations

One or more equations did not get rendered due to their size.

source

instance Pi.distribMulAction' {I : Type u} {f : I → Type v} {g : I → Type u_1} {m : (i : I) → Monoid (f i)} {n : (i : I) → AddMonoid (g i)} [(i : I) → DistribMulAction (f i) (g i)] :

DistribMulAction ((i : I) → f i) ((i : I) → g i)

Equations

One or more equations did not get rendered due to their size.

source

theorem Pi.single_smul {I : Type u} {f : I → Type v} {α : Type u_1} [Monoid α] [(i : I) → AddMonoid (f i)] [(i : I) → DistribMulAction α (f i)] [DecidableEq I] (i : I) (r : α) (x : f i) :

Pi.single i (r • x) = r • Pi.single i x

source

theorem Pi.single_smul' {I : Type u} {α : Type u_1} {β : Type u_2} [Monoid α] [AddMonoid β] [DistribMulAction α β] [DecidableEq 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 where Lean fails to apply Pi.single_smul.

source

theorem Pi.single_smul₀ {I : Type u} {f : I → Type v} {g : I → Type u_1} [(i : I) → MonoidWithZero (f i)] [(i : I) → AddMonoid (g i)] [(i : I) → DistribMulAction (f i) (g i)] [DecidableEq I] (i : I) (r : f i) (x : g i) :

Pi.single i (r • x) = Pi.single i r • Pi.single i x

source

instance Pi.mulDistribMulAction {I : Type u} {f : I → Type v} (α : Type u_1) {m : Monoid α} {n : (i : I) → Monoid (f i)} [(i : I) → MulDistribMulAction α (f i)] :

MulDistribMulAction α ((i : I) → f i)

Equations

Pi.mulDistribMulAction α = let src := Pi.mulAction α; MulDistribMulAction.mk (_ : ∀ (x : α) (x_1 x_2 : (i : I) → f i), x • (x_1 * x_2) = x • x_1 * x • x_2) (_ : ∀ (x : α), x • 1 = 1)

source

instance Pi.mulDistribMulAction' {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) → MulDistribMulAction (f i) (g i)] :

MulDistribMulAction ((i : I) → f i) ((i : I) → g i)

Equations

Pi.mulDistribMulAction' = MulDistribMulAction.mk (_ : ∀ (r : (i : I) → f i) (x y : (i : I) → g i), r • (x * y) = r • x * r • y) (_ : ∀ (r : (i : I) → f i), r • 1 = 1)

source

instance Function.hasVAdd {ι : Type u_1} {R : Type u_2} {M : Type u_3} [VAdd R M] :

VAdd R (ι → M)

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

Equations

Function.hasVAdd = Pi.instVAdd

source

instance Function.hasSMul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [SMul R M] :

SMul R (ι → M)

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

Equations

Function.hasSMul = Pi.instSMul

source

theorem Function.vaddCommClass.proof_1 {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [VAdd α M] [VAdd β M] [VAddCommClass α β M] :

VAddCommClass α β (ι → M)

source

instance Function.vaddCommClass {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [VAdd α M] [VAdd β M] [VAddCommClass α β M] :

VAddCommClass α β (ι → M)

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

Equations

@Function.vaddCommClass = @Function.vaddCommClass.proof_1

source

instance Function.smulCommClass {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_4} [SMul α M] [SMul β M] [SMulCommClass α β M] :

SMulCommClass α β (ι → M)

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

Equations

@Function.smulCommClass = @Function.smulCommClass.proof_1

source

theorem Function.update_vadd {I : Type u} {f : I → Type v} {α : Type u_1} [(i : I) → VAdd α (f i)] [DecidableEq 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₁

source

theorem Function.update_smul {I : Type u} {f : I → Type v} {α : Type u_1} [(i : I) → SMul α (f i)] [DecidableEq 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₁

source

theorem Set.piecewise_vadd {I : Type u} {f : I → Type v} {α : Type u_1} [(i : I) → VAdd α (f i)] (s : Set I) [(i : I) → Decidable (i ∈ s)] (c : α) (f₁ : (i : I) → f i) (g₁ : (i : I) → f i) :

Set.piecewise s (c +ᵥ f₁) (c +ᵥ g₁) = c +ᵥ Set.piecewise s f₁ g₁

source

theorem Set.piecewise_smul {I : Type u} {f : I → Type v} {α : Type u_1} [(i : I) → SMul α (f i)] (s : Set I) [(i : I) → Decidable (i ∈ s)] (c : α) (f₁ : (i : I) → f i) (g₁ : (i : I) → f i) :

Set.piecewise s (c • f₁) (c • g₁) = c • Set.piecewise s f₁ g₁

source

theorem Function.extend_vadd {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [VAdd R γ] (r : R) (f : α → β) (g : α → γ) (e : β → γ) :

Function.extend f (r +ᵥ g) (r +ᵥ e) = r +ᵥ Function.extend f g e

source

theorem Function.extend_smul {R : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [SMul R γ] (r : R) (f : α → β) (g : α → γ) (e : β → γ) :

Function.extend f (r • g) (r • e) = r • Function.extend f g e