Documentation

Mathlib.Algebra.Module.Pi

Pi instances for modules #

This file defines instances for module and related structures on Pi Types

theorem IsSMulRegular.pi {I : Type u} {f : IType 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 : IType 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 : IType v} {g : IType 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 : IType 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 : IType v} {g : IType 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 : IType v) (α : Type u_1) {r : Semiring α} {m : (i : I) → AddCommMonoid (f i)} [(i : I) → Module α (f i)] :
Module α ((i : I) → f i)
Equations
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
instance Pi.module' {I : Type u} {f : IType v} {g : IType 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 : IType 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