eval₂_coe — Mathlib

English

For any r ∈ R, eval₂ φ a (C r) = φ r.

Русский

Для любого r ∈ R, eval₂ φ a (C r) = φ r.

LaTeX

$$$\text{eval}_2 φ\, a\, (\mathrm{C} r) = φ(r)$$$

Lean4

@[simp]
theorem eval₂_coe (f : Polynomial R) : eval₂ φ a f = f.eval₂ φ a :=
  by
  let g : MvPolynomial Unit R := (MvPolynomial.pUnitAlgEquiv R).symm f
  have : f = MvPolynomial.pUnitAlgEquiv R g := by simp only [g, ← AlgEquiv.symm_apply_eq]
  simp only [this, PowerSeries.eval₂, MvPolynomial.eval₂_const_pUnitAlgEquiv]
  rw [← MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPowerSeries.eval₂_coe]

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