commute_T — 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

theorem commute_T (n : ℤ) (f : R[T;T⁻¹]) : Commute (T n) f :=
  f.induction_on' (fun _ _ Tp Tq => Commute.add_right Tp Tq) fun m a =>
    show T n * _ = _ by
      rw [T, T, ← single_eq_C, single_mul_single, single_mul_single, single_mul_single]
      simp [add_comm]

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