instFunLike — Mathlib

English

There is a canonical function-like structure on Poly α given by the projection onto coefficient data; i.e., Poly α carries a natural FunLike structure.

Русский

У Poly α существует каноническая структура типа FunLike, задаваемая проекцией на данные коэффициентов.

LaTeX

$$$\text{Poly}(\alpha)$ is equipped with a canonical FunLike structure via the projection $\text{val}$.$$

Lean4

instance instFunLike : FunLike (Poly α) (α → ℕ) ℤ :=
  ⟨Subtype.val, Subtype.val_injective⟩

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