invert_T

Mathlib.Algebra.Polynomial.Laurent

URI: https://scilib.ai/kg/mathlib#LaurentPolynomial.invert_T

English

For any LaurentPolynomial R, and integer n, invert f n = f(-n).

Русский

Для любого Лаурентового полинома f и целого n: invert f n = f(-n).

LaTeX

$$$\\mathrm{invert}(f)(n) = f(-n) \\quad$ для всех $n \\in \\mathbb{Z}$.$$

Lean4

@[simp]
theorem invert_T (n : ℤ) : invert (T n : R[T;T⁻¹]) = T (-n) :=
  AddMonoidAlgebra.domCongr_single _ _ _ _ _

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

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

Разделы

Аффилиация

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