coeFnRingHom — Mathlib

English

There is a natural RingHom from LocallyConstant(X,Y) to X→Y given by evaluation at each point, i.e., the function that sends f to the map x ↦ f(x).

Русский

Существует естественный кольцевой однородник из LocallyConstant(X,Y) в X→Y, отправляющий f в отображение x ↦ f(x).

LaTeX

$$$\\operatorname{coeFnRingHom}: \\operatorname{LocallyConstant}(X,Y) \\to_{\mathrm{Ring}} (X \\to Y)$$$

Lean4

/-- `DFunLike.coe` as a `RingHom`. -/
@[simps!]
def coeFnRingHom [Semiring Y] : LocallyConstant X Y →+* X → Y
    where
  toMonoidHom := coeFnMonoidHom
  __ := coeFnAddMonoidHom

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