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

instance Pi.module (I : Type u) (f : I → Type v) (α : Type u_1) {r : Semiring α} {m : (i : I) → AddCommMonoid (f i)} [(i : I) → Module α (f i)] : Module α ((i : I) → f i)

Equations

• Pi.module I f α = { toDistribMulAction := Pi.distribMulAction α, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

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

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 := ⋯ }