Pi instances for ring #
This file defines instances for ring, semiring and related structures on Pi Types
A family of non-unital ring homomorphisms f a : γ →ₙ+* β a
defines a non-unital ring
homomorphism Pi.nonUnitalRingHom f : γ →+* Π a, β a
given by
Pi.nonUnitalRingHom f x b = f b x
.
Instances For
A family of ring homomorphisms f a : γ →+* β a
defines a ring homomorphism
Pi.ringHom f : γ →+* Π a, β a
given by Pi.ringHom f x b = f b x
.
Instances For
Evaluation of functions into an indexed collection of non-unital rings at a point is a
non-unital ring homomorphism. This is Function.eval
as a NonUnitalRingHom
.
Instances For
Function.const
as a NonUnitalRingHom
.
Instances For
Non-unital ring homomorphism between the function spaces I → α
and I → β
, induced by a
non-unital ring homomorphism f
between α
and β
.
Instances For
Evaluation of functions into an indexed collection of rings at a point is a ring
homomorphism. This is Function.eval
as a RingHom
.
Instances For
Function.const
as a RingHom
.
Instances For
Ring homomorphism between the function spaces I → α
and I → β
, induced by a ring
homomorphism f
between α
and β
.