eval₂_C_mul_T_n

Mathlib.Algebra.Polynomial.Laurent

URI: https://scilib.ai/kg/mathlib#LaurentPolynomial.eval₂_C_mul_T_n

← MathLib Explorer

English

For r ∈ R and n ∈ ℕ, eval₂ f x (C r · T^n) = f r · x^n.

Русский

Для r ∈ R и n ∈ ℕ: eval₂ f x (C r · T^n) = f r · x^n.

LaTeX

$$$\\mathrm{eval_2}(f,x)(C r \\cdot T^{n}) = f r \\cdot x^{n}$ for $r\\in R$, $n\\in\\mathbb{N}$.$$

Lean4

theorem eval₂_C_mul_T_n (r : R) (n : ℕ) : eval₂ f x (C r * T n) = f r * x ^ n := by
  rw [← Polynomial.toLaurent_C_mul_T, eval₂_toLaurent, eval₂_monomial]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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