eval₂_T_neg_n

Mathlib.Algebra.Polynomial.Laurent

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

← MathLib Explorer

English

For n ∈ ℕ, eval₂ f x (T(-n)) = x^{-1})^n.

Русский

Для n ∈ ℕ: eval₂ f x (T(-n)) = x^{-1})^n.

LaTeX

$$$\\mathrm{eval_2}(f,x)(T^{-n}) = (x^{-1})^n$ for $n \\ge 0$.$$

Lean4

theorem eval₂_T_neg_n (n : ℕ) : eval₂ f x (T (-n)) = x⁻¹ ^ n :=
  by
  rw [← mk'_one_X_pow]
  unfold eval₂
  rw [IsLocalization.lift_mk'_spec, map_one, coe_eval₂RingHom, eval₂_X_pow, ← mul_pow, Units.mul_inv, one_pow]

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

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

Разделы

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

Аффилиация

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