evalRingHom — Mathlib

English

Evaluation at a fixed x gives a RingHom from LocallyConstant(X,Y) to Y, i.e., the map f ↦ f(x) respects addition and multiplication.

Русский

Оценка по фиксированной точке x задаёт RingHom от LocallyConstant(X,Y) к Y, т.е. отображение f ↦ f(x) сохраняет сложение и умножение.

LaTeX

$$$\operatorname{evalRingHom}(x): \operatorname{LocallyConstant}(X,Y) \to_{\mathrm{Ring}} Y$$$

Lean4

/-- Evaluation as a `RingHom` -/
@[simps!]
def evalRingHom [Semiring Y] (x : X) : LocallyConstant X Y →+* Y :=
  (Pi.evalRingHom _ x).comp coeFnRingHom

Похожие утверждения