HepLean Documentation

Mathlib.Algebra.GroupWithZero.Action.Pi

Pi instances for multiplicative actions with zero #

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

See also #

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