map_toPoly — Mathlib

English

The polynomial underlying the image cubic equals the polynomial map of the original polynomial.

Русский

Полином-подтип исходного кубического полинома совпадает с отображением полинома через φ.

LaTeX

$$$$ (\\mathrm{Cubic.map}\\varphi\\,P).toPoly = \\mathrm{Polynomial.map}\\varphi\\,P.toPoly. $$$$

Lean4

theorem map_toPoly : (map φ P).toPoly = Polynomial.map φ P.toPoly := by
  simp only [map, toPoly, map_C, map_X, Polynomial.map_add, Polynomial.map_mul, Polynomial.map_pow]

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