eval₂_T_n

Mathlib.Algebra.Polynomial.Laurent

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

English

For n ∈ ℕ, eval₂ f x (T^n) = x^n, i.e. the variable T evaluates to x.

Русский

Для n ∈ ℕ: eval₂ f x (T^n) = x^n, то есть переменная T принимает значение x.

LaTeX

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

Lean4

theorem eval₂_T_n (n : ℕ) : eval₂ f x (T n) = x ^ n := by
  rw [← Polynomial.toLaurent_X_pow, eval₂_toLaurent, eval₂_X_pow]

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

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

Разделы

Аффилиация

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