coe_pow — Mathlib

English

The embedding commutes with multiplication: the image of φ^n is the nth power of the image of φ in PowerSeries R.

Русский

Умножение полиномов под встроением сохраняется: образ φ^n в PowerSeries равен (образ φ)^n.

LaTeX

$$$((\\varphi^n : R[X]) : \\mathrm{PowerSeries}(R)) = (\\varphi : \\mathrm{PowerSeries}(R))^n$$$

Lean4

@[simp, norm_cast]
theorem coe_pow (n : ℕ) : ((φ ^ n : R[X]) : PowerSeries R) = (φ : PowerSeries R) ^ n :=
  coeToPowerSeries.ringHom.map_pow _ _

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