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.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.module'
{I : Type u}
{f : I → Type v}
{g : I → Type u_1}
{r : (i : I) → Semiring (f i)}
{m : (i : I) → AddCommMonoid (g i)}
[(i : I) → Module (f i) (g i)]
:
Module ((i : I) → f i) ((i : I) → g i)
Equations
- Pi.module' = { toDistribMulAction := Pi.distribMulAction', add_smul := ⋯, zero_smul := ⋯ }