mathlib documentation

algebra.ring.pi

Pi instances for ring

This file defines instances for ring, semiring and related structures on Pi Types

@[instance]
def pi.mul_zero_class {I : Type u} {f : I → Type v} [Π (i : I), mul_zero_class (f i)] :
mul_zero_class (Π (i : I), f i)

Equations
@[instance]
def pi.distrib {I : Type u} {f : I → Type v} [Π (i : I), distrib (f i)] :
distrib (Π (i : I), f i)

Equations
@[instance]
def pi.semiring {I : Type u} {f : I → Type v} [Π (i : I), semiring (f i)] :
semiring (Π (i : I), f i)

Equations
@[instance]
def pi.comm_semiring {I : Type u} {f : I → Type v} [Π (i : I), comm_semiring (f i)] :
comm_semiring (Π (i : I), f i)

Equations
@[instance]
def pi.ring {I : Type u} {f : I → Type v} [Π (i : I), ring (f i)] :
ring (Π (i : I), f i)

Equations
@[instance]
def pi.comm_ring {I : Type u} {f : I → Type v} [Π (i : I), comm_ring (f i)] :
comm_ring (Π (i : I), f i)

Equations
def pi.ring_hom {α : Type u} {β : α → Type v} [R : Π (a : α), semiring (β a)] {γ : Type w} [semiring γ] :
(Π (a : α), γ →+* β a)→+* Π (a : α), β a)

A family of ring homomorphisms f a : γ →+* β a defines a ring homomorphism pi.ring_hom f : γ →+* Π a, β a given by pi.ring_hom f x b = f b x.

Equations
@[simp]
theorem pi.ring_hom_apply {α : Type u} {β : α → Type v} [R : Π (a : α), semiring (β a)] {γ : Type w} [semiring γ] (f : Π (a : α), γ →+* β a) (g : γ) (a : α) :
(pi.ring_hom f) g a = (f a) g

def ring_hom.apply {I : Type u_1} (f : I → Type u_2) [Π (i : I), semiring (f i)] (i : I) :
(Π (i : I), f i) →+* f i

Evaluation of functions into an indexed collection of monoids at a point is a monoid homomorphism.

Equations
@[simp]
theorem ring_hom.apply_apply {I : Type u_1} (f : I → Type u_2) [Π (i : I), semiring (f i)] (i : I) (g : Π (i : I), f i) :
(ring_hom.apply f i) g = g i