mathlib documentation

algebra.module.pi

Pi instances for modules #

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), has_scalar α (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), smul_with_zero α (f i)] :
smul_with_zero α (Π (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) [monoid_with_zero α] [Π (i : I), has_zero (f i)] [Π (i : I), mul_action_with_zero α (f i)] :
mul_action_with_zero α (Π (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), module α (f i)] :
module α (Π (i : I), f i)
Equations
@[protected, instance]
def function.module (I : Type u) (α : Type u_1) (β : Type u_2) [semiring α] [add_comm_monoid β] [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
@[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), module α (f i)] [∀ (i : I), no_zero_smul_divisors α (f i)] :
no_zero_smul_divisors α (Π (i : I), f i)