polynomial_map_coe — Mathlib

English

For any φ: U →+* V and f ∈ Polynomial U, the polynomial map commutes with embedding into power series: Polynomial.map φ f, treated as a power series, equals PowerSeries.map φ f.

Русский

Для φ: U →+* V и f ∈ Polynomial U отображение полиномов коммутирует с вложением в степенные ряды: Polynomial.map φ f в PowerSeries одинаково с PowerSeries.map φ f.

LaTeX

$$$(Polynomial.map\\ \\varphi\\ f).toPowerSeries = PowerSeries.map \\varphi f$$$

Lean4

@[simp]
theorem polynomial_map_coe {U V : Type*} [CommSemiring U] [CommSemiring V] {φ : U →+* V} {f : Polynomial U} :
    Polynomial.map φ f = PowerSeries.map φ f := by
  ext
  simp

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