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
- Pi.smulWithZero α = let __src := Pi.instSMul; SMulWithZero.mk ⋯
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' = let __src := Pi.smul'; 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
- Pi.mulActionWithZero α = let __src := Pi.mulAction α; let __src_1 := Pi.smulWithZero α; MulActionWithZero.mk ⋯ ⋯
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' = let __src := Pi.mulAction'; let __src_1 := Pi.smulWithZero'; 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) => β) α
instance
Pi.noZeroSMulDivisors
{I : Type u}
{f : I → Type v}
(α : Type u_1)
[Semiring α]
[(i : I) → AddCommMonoid (f i)]
[(i : I) → Module α (f i)]
[∀ (i : I), NoZeroSMulDivisors α (f i)]
:
NoZeroSMulDivisors α ((i : I) → f i)
Equations
- ⋯ = ⋯
instance
Function.noZeroSMulDivisors
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Semiring α]
[AddCommMonoid β]
[Module α β]
[NoZeroSMulDivisors α β]
:
NoZeroSMulDivisors α (ι → β)
A special case of Pi.noZeroSMulDivisors for non-dependent types. Lean struggles to
synthesize this instance by itself elsewhere in the library.
Equations
- ⋯ = ⋯