ringHom_apply — Mathlib

English

For every polynomial φ, the image under the polynomial-to-power-series embedding equals φ considered as a power series.

Русский

Для каждого полинома φ изображение его под встраиванием в ряд степенных равно φ, рассматриваемому как степенной ряд.

LaTeX

$$$\\text{coeToPowerSeries.ringHom }\\phi = \\phi$$$

Lean4

@[simp]
theorem ringHom_apply : coeToPowerSeries.ringHom φ = φ :=
  rfl

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