Pi instances for modules #
This file defines instances for module and related structures on Pi Types
theorem
IsSMulRegular.pi
{I : Type u}
{f : I → Type v}
{α : Type u_1}
[(i : I) → SMul α (f i)]
{k : α}
(hk : ∀ (i : I), IsSMulRegular (f i) k)
:
IsSMulRegular ((i : I) → f i) k
instance
Pi.smulWithZero
{I : Type u}
{f : I → Type v}
(α : Type u_1)
[Zero α]
[(i : I) → Zero (f i)]
[(i : I) → SMulWithZero α (f i)]
:
SMulWithZero α ((i : I) → f i)
Equations
instance
Pi.smulWithZero'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
[(i : I) → Zero (g i)]
[(i : I) → Zero (f i)]
[(i : I) → SMulWithZero (g i) (f i)]
:
SMulWithZero ((i : I) → g i) ((i : I) → f i)
Equations
- Pi.smulWithZero' = SMulWithZero.mk ⋯
instance
Pi.mulActionWithZero
{I : Type u}
{f : I → Type v}
(α : Type u_1)
[MonoidWithZero α]
[(i : I) → Zero (f i)]
[(i : I) → MulActionWithZero α (f i)]
:
MulActionWithZero α ((i : I) → f i)
Equations
instance
Pi.mulActionWithZero'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
[(i : I) → MonoidWithZero (g i)]
[(i : I) → Zero (f i)]
[(i : I) → MulActionWithZero (g i) (f i)]
:
MulActionWithZero ((i : I) → g i) ((i : I) → f i)
Equations
- Pi.mulActionWithZero' = MulActionWithZero.mk ⋯ ⋯
instance
Pi.Function.module
(I : Type u)
(α : Type u_1)
(β : Type u_2)
[Semiring α]
[AddCommMonoid β]
[Module α β]
:
Module α (I → β)
A special case of Pi.module for non-dependent types. Lean struggles to elaborate
definitions elsewhere in the library without this.
Equations
- Pi.Function.module I α β = Pi.module I (fun (a : I) => β) α