eval₂_monomial

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

For a monomial monomial n r, eval₂ f x yields f r times x raised to n.

Русский

Для монома monomial n r вычисление eval₂ даёт f r умножить на x^n.

LaTeX

$$$ (monomial\\ n\\ r).eval\\_2 f x = f r \\cdot x^n $$$

Lean4

@[simp]
theorem eval₂_monomial {n : ℕ} {r : R} : (monomial n r).eval₂ f x = f r * x ^ n := by simp [eval₂_eq_sum]

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

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

Разделы

Аффилиация

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