single_eq_C_mul_T — Mathlib

English

The Laurent monomial with exponent n and coefficient r factors as the product of the constant C r with T n: Finsupp.single n r = C r · T n.

Русский

Лаурентовский моном с экспонентой n и коэффициентом r равен произведению константы C r на T n: Finsupp.single n r = C r · T n.

LaTeX

$$$Finsupp.single n\\, r = C\\, r * T\\, n$$$

Lean4

@[simp]
theorem single_eq_C_mul_T (r : R) (n : ℤ) : (Finsupp.single n r : R[T;T⁻¹]) = (C r * T n : R[T;T⁻¹]) := by
  simp [C, T, single_mul_single]
    -- This lemma locks in the right changes and is what Lean proved directly.
    -- The actual `simp`-normal form of a Laurent monomial is `C a * T n`, whenever it can be reached.

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