invOf_T

Mathlib.Algebra.Polynomial.Laurent

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

English

The inverse of T(n) is T(-n): ⅟(T n) = T(-n).

Русский

Обратное к T(n) равно T(-n).

LaTeX

$$$ ⅟(T n : R[T;T^{-1}]) = T(-n) $$$

Lean4

@[simp]
theorem invOf_T (n : ℤ) : ⅟(T n : R[T;T⁻¹]) = T (-n) :=
  rfl

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

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

Разделы

Аффилиация

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