T_apply — Mathlib

English

The coefficient of the Laurent monomial T(n) at exponent m is 1 if m = n and 0 otherwise.

Русский

Коэффициент лаурентовского монома $T(n)$ при степени $m$ равен 1, если $m=n$, и 0 в противном случае.

LaTeX

$$$(T\\ n)\\ m = \\begin{cases}1, & m=n \\\\ 0, & m\\neq n\\end{cases}$$$

Lean4

@[simp]
theorem T_apply (m n : ℤ) : (T n : R[T;T⁻¹]) m = if n = m then 1 else 0 :=
  Finsupp.single_apply

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