# mathlib3documentation

algebra.module.pi

# Pi instances for modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem is_smul_regular.pi {I : Type u} {f : I Type v} {α : Type u_1} [Π (i : I), (f i)] {k : α} (hk : (i : I), is_smul_regular (f i) k) :
is_smul_regular (Π (i : I), f i) k
@[protected, instance]
def pi.smul_with_zero {I : Type u} {f : I Type v} (α : Type u_1) [has_zero α] [Π (i : I), has_zero (f i)] [Π (i : I), (f i)] :
(Π (i : I), f i)
Equations
@[protected, instance]
def pi.smul_with_zero' {I : Type u} {f : I Type v} {g : I Type u_1} [Π (i : I), has_zero (g i)] [Π (i : I), has_zero (f i)] [Π (i : I), smul_with_zero (g i) (f i)] :
smul_with_zero (Π (i : I), g i) (Π (i : I), f i)
Equations
@[protected, instance]
def pi.mul_action_with_zero {I : Type u} {f : I Type v} (α : Type u_1) [Π (i : I), has_zero (f i)] [Π (i : I), (f i)] :
(Π (i : I), f i)
Equations
@[protected, instance]
def pi.mul_action_with_zero' {I : Type u} {f : I Type v} {g : I Type u_1} [Π (i : I), monoid_with_zero (g i)] [Π (i : I), has_zero (f i)] [Π (i : I), mul_action_with_zero (g i) (f i)] :
mul_action_with_zero (Π (i : I), g i) (Π (i : I), f i)
Equations
@[protected, instance]
def pi.module (I : Type u) (f : I Type v) (α : Type u_1) {r : semiring α} {m : Π (i : I), add_comm_monoid (f i)} [Π (i : I), (f i)] :
(Π (i : I), f i)
Equations
@[protected, instance]
def function.module (I : Type u) (α : Type u_1) (β : Type u_2) [semiring α] [ β] :
(I β)

A special case of pi.module for non-dependent types. Lean struggles to elaborate definitions elsewhere in the library without this.

Equations
• β = (λ (ᾰ : I), β) α
@[protected, instance]
def pi.module' {I : Type u} {f : I Type v} {g : I Type u_1} {r : Π (i : I), semiring (f i)} {m : Π (i : I), add_comm_monoid (g i)} [Π (i : I), module (f i) (g i)] :
module (Π (i : I), f i) (Π (i : I), g i)
Equations
@[protected, instance]
def pi.no_zero_smul_divisors {I : Type u} {f : I Type v} (α : Type u_1) {r : semiring α} {m : Π (i : I), add_comm_monoid (f i)} [Π (i : I), (f i)] [ (i : I), (f i)] :
(Π (i : I), f i)
@[protected, instance]
def function.no_zero_smul_divisors {ι : Type u_1} {α : Type u_2} {β : Type u_3} {r : semiring α} {m : add_comm_monoid β} [ β]  :
β)

A special case of pi.no_zero_smul_divisors for non-dependent types. Lean struggles to synthesize this instance by itself elsewhere in the library.