toLaurent_X — Mathlib

English

For every integer n and Laurent polynomial f, T(n) commutes with f: T(n) f = f T(n).

Русский

Для каждого целого числа $n$ и лаурентовского многочлена $f$ выполняется $T(n) f = f T(n)$.

LaTeX

$$Commute\\ (T(n))\\ (f)$$

Lean4

@[simp]
theorem _root_.Polynomial.toLaurent_X : (toLaurent Polynomial.X : R[T;T⁻¹]) = T 1 :=
  by
  have : (Polynomial.X : R[X]) = monomial 1 1 := by simp [← C_mul_X_pow_eq_monomial]
  simp [this, Polynomial.toLaurent_C_mul_T]

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