eval₂_C_X_eq_coe — Mathlib

English

Evaluating a polynomial φ at the constants C and the indeterminate X yields φ viewed as a power series.

Русский

Оценка полинома φ по константам C и переменной X даёт φ, рассматриваемый как ряд степенных.

LaTeX

$$$\\varphi.{\\mathrm{eval}}_{2} \\;\\mathrm{PowerSeries.C} \\; \\mathrm{PowerSeries.X} = \\uparrow\\varphi$$$

Lean4

theorem eval₂_C_X_eq_coe : φ.eval₂ PowerSeries.C PowerSeries.X = ↑φ :=
  by
  nth_rw 2 [← eval₂_C_X (p := φ)]
  rw [← coeToPowerSeries.ringHom_apply, eval₂_eq_sum_range, eval₂_eq_sum_range, map_sum]
  apply Finset.sum_congr rfl
  intros
  rw [map_mul, map_pow, coeToPowerSeries.ringHom_apply, coeToPowerSeries.ringHom_apply, coe_C, coe_X]

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