coeFnRingHom — Mathlib

English

There is a RingHom from C(α, β) to α → β given by the evaluation map x ↦ f(x); this respects ring operations and the topological semiring structure on β.

Русский

Существует RingHom от C(α, β) в α → β, задаваемый по точке x ↦ f(x); он сохраняет операции кольца и структуру топологического полукольца на β.

LaTeX

$$$ C(\alpha, \beta) \to \alpha \to \beta \text{ via } f \mapsto (x \mapsto f(x)) \text{ is a RingHom}. $$$

Lean4

/-- Coercion to a function as a `RingHom`. -/
@[simps!]
def coeFnRingHom {α : Type*} {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [Semiring β]
    [IsTopologicalSemiring β] : C(α, β) →+* α → β :=
  { (coeFnMonoidHom : C(α, β) →* _), (coeFnAddMonoidHom : C(α, β) →+ _) with }

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