Pi instances for multiplicative actions with zero #
This file defines instances for MulActionWithZero
and related structures on Pi
types.
See also #
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
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
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
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' = 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)
:
theorem
Pi.single_smul'
{I : Type u}
{α : Type u_1}
{β : Type u_2}
[Monoid α]
[AddMonoid β]
[DistribMulAction α β]
[DecidableEq I]
(i : I)
(r : α)
(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)
:
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
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 ⋯ ⋯