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 (_ : ∀ (x : (i : I) → f i), 0 • x = 0)

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 (_ : ∀ (x : (i : I) → f i), 0 • x = 0)

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 (_ : ∀ (a : α), a • 0 = 0) (_ : ∀ (m : (i : I) → f i), 0 • m = 0)

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 (_ : ∀ (a : (i : I) → g i), a • 0 = 0) (_ : ∀ (m : (i : I) → f i), 0 • m = 0)

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 α = let src := Pi.distribMulAction α; Module.mk (_ : ∀ (x x_1 : α) (x_2 : (i : I) → f i), (x + x_1) • x_2 = x • x_2 + x_1 • x_2) (_ : ∀ (x : (i : I) → f i), 0 • x = 0)

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 => β) α

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' = Module.mk (_ : ∀ (r s : (i : I) → f i) (x : (i : I) → g i), (r + s) • x = r • x + s • x) (_ : ∀ (x : (i : I) → g i), 0 • x = 0)

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

• @Pi.noZeroSMulDivisors = @Pi.noZeroSMulDivisors.proof_1

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

• @Function.noZeroSMulDivisors = @Function.noZeroSMulDivisors.proof_1