eta — Mathlib

English

The canonical map sending a polynomial to its finsupp representation is an isomorphism, i.e., Polynomial.ofFinsupp maps back to the original polynomial.

Русский

Каноническое отображение полинома в его представление через finsupp является изоморфизмом; Polynomial.ofFinsupp обратимо восстанавливает исходный полином.

LaTeX

$$$ \eta_f : \text{Polynomial.ofFinsupp} (f.toFinsupp) = f $$$

Lean4

@[simp]
theorem eta (f : R[X]) : Polynomial.ofFinsupp f.toFinsupp = f := by constructor

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