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
- pi.mul_zero_class = {mul := has_mul.mul pi.has_mul, zero := 0, zero_mul := _, mul_zero := _}
@[instance]
Equations
- pi.distrib = {mul := has_mul.mul pi.has_mul, add := has_add.add pi.has_add, left_distrib := _, right_distrib := _}
@[instance]
def
pi.semiring
{I : Type u}
{f : I → Type v}
[Π (i : I), semiring (f i)] :
semiring (Π (i : I), f i)
Equations
- pi.semiring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
@[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
- pi.comm_semiring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
Equations
- pi.ring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg pi.has_neg, add_left_neg := _, add_comm := _, mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
@[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
- pi.comm_ring = {add := has_add.add pi.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg pi.has_neg, add_left_neg := _, add_comm := _, mul := has_mul.mul pi.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
def
pi.ring_hom
{α : Type u}
{β : α → Type v}
[R : Π (a : α), semiring (β a)]
{γ : Type w}
[semiring γ]
(f : Π (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.
@[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
- ring_hom.apply f i = {to_fun := (monoid_hom.apply f i).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[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