English
For each integer n, the Laurent monomial T(n) is the monomial with coefficient 1 at exponent n and 0 elsewhere.
Русский
Для каждого целого \(n\) лаурентовский моном T(n) есть мономом с коэффициентом 1 при степени \(n\) и нулём в остальных местах.
LaTeX
$$$T(n) = Finsupp.single\\ n\\, 1$$$
Lean4
/-- The function `n ↦ T ^ n`, implemented as a sequence `ℤ → R[T;T⁻¹]`.
Using directly `T ^ n` does not work, since we want the exponents to be of Type `ℤ` and there
is no `ℤ`-power defined on `R[T;T⁻¹]`. Using that `T` is a unit introduces extra coercions.
For these reasons, the definition of `T` is as a sequence. -/
def T (n : ℤ) : R[T;T⁻¹] :=
Finsupp.single n 1
