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

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 ⋯

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 ⋯

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 ⋯

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 ⋯

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

• Pi.distribMulAction α = let __src := Pi.mulAction α; let __src_1 := Pi.distribSMul α; DistribMulAction.mk ⋯ ⋯

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

• Pi.distribMulAction' = let __src := Pi.mulAction'; let __src_1 := Pi.distribSMul'; DistribMulAction.mk ⋯ ⋯

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

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.

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

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 ⋯ ⋯

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 ⋯ ⋯