Theorems · Definition · ring theory

Pi.evalRingHom

{I : Type u} → (f : I → Type v) → [inst : (i : I) → NonAssocSemiring (f i)] → (i : I) → ((i : I) → f i) →+* f i

Evaluation of functions into an indexed collection of rings at a point is a ring homomorphism. This is Function.eval as a RingHom.

Defined in

Mathlib.Algebra.Ring.Pi

Cited by

44 results in Mathlib

Foundations

Depth 15 from the axioms · uses Quot.sound

Assumes

NonAssocSemiring