eval₂_eq_sum

Mathlib.Algebra.Polynomial.Eval.Defs

URI: https://scilib.ai/kg/mathlib#Polynomial.eval₂_eq_sum

English

If f = g, s = t, φ = ψ, then eval₂ f s φ = eval₂ g t ψ.

Русский

Если f = g, s = t, φ = ψ, тогда eval₂ f s φ = eval₂ g t ψ.

LaTeX

$$$ eval\\_2\\ f\\ s\\ φ = eval\\_2\\ g\\ t\\ ψ \\leftarrow\\leftarrow (f=g) (s=t) (φ=ψ) $$$

Lean4

theorem eval₂_eq_sum {f : R →+* S} {x : S} : p.eval₂ f x = p.sum fun e a => f a * x ^ e := by rw [eval₂_def]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru