toLaurent_C_mul_T — Mathlib

English

Each T(n) is a unit in the Laurent polynomial ring, with inverse T(-n).

Русский

Каждый T(n) является единицей в кольце лаурентовских многочленов, имеет обратный T(-n).

LaTeX

$$$T(n) \\cdot T(-n) = 1$ and $T(-n) \\cdot T(n) = 1$$$

Lean4

@[simp]
theorem _root_.Polynomial.toLaurent_C_mul_T (n : ℕ) (r : R) :
    (toLaurent (Polynomial.monomial n r) : R[T;T⁻¹]) = C r * T n :=
  show Finsupp.mapDomain (↑) (monomial n r).toFinsupp = (C r * T n : R[T;T⁻¹]) by
    rw [toFinsupp_monomial, Finsupp.mapDomain_single, single_eq_C_mul_T]

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