coeFun — Mathlib

English

There is a canonical way to view a polynomial sequence as a function sending indices to polynomials: i ↦ S i.

Русский

Существует канонический способ рассматривать последовательность многочленов как функцию, которая сопоставляет каждому индексу i соответствующий многочлен S i.

LaTeX

$$$\text{There exists a canonical coercion } S: \mathbb{N} \to (\text{ Polynomial } R) \text{ given by } S(i) = S_i$$$

Lean4

/-- Make `S i` mean `S.elems' i`. -/
instance coeFun [Semiring R] : CoeFun (Sequence R) (fun _ ↦ ℕ → R[X]) :=
  ⟨Sequence.elems'⟩

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