T_mul — Mathlib

English

Let R be a semiring. For every n ∈ Z and every f in R[T;T^{-1}], the Laurent monomial T^n commutes with f: T^n f = f T^n.

Русский

Пусть R — полукольцо. Для произвольного n ∈ ℤ и любого f ∈ R[T;T^{-1}] верно, что T^n коммутирует с f: T^n f = f T^n.

LaTeX

$$$\forall n \in \mathbb{Z}, \forall f \in R[T;T^{-1}]:\ T^{n} f = f T^{n}$$$

Lean4

@[simp]
theorem T_mul (n : ℤ) (f : R[T;T⁻¹]) : T n * f = f * T n :=
  (commute_T n f).eq

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