mul_T_assoc — Mathlib

English

In the Laurent polynomial ring, the product with two monomials is associative with the sum of exponents: f T(m) T(n) = f T(m+n).

Русский

В кольце лаурентовских многочленов произведение с двумя мономами совместимо: f T(m) T(n) = f T(m+n).

LaTeX

$$$f * T\\,m * T\\,n = f * T\\,(m + n)$$$

Lean4

/-- The `simp` version of `mul_assoc`, in the presence of `T`'s. -/
@[simp]
theorem mul_T_assoc (f : R[T;T⁻¹]) (m n : ℤ) : f * T m * T n = f * T (m + n) := by simp [← T_add, mul_assoc]

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