C_apply — Mathlib

English

For any t in R and any integer n, the coefficient of the constant Laurent polynomial C t at exponent n is t if n = 0 and 0 otherwise.

Русский

Для любого t в R и любой целой $n$ коэффициент константного лаурентовского многочлена C t при степени $n$ равен t, если $n=0$, и равен 0 в противном случае.

LaTeX

$$$C t n = \\begin{cases} t, & n=0 \\\\ 0, & n\\neq 0 \\end{cases}$$$

Lean4

@[simp]
theorem C_apply (t : R) (n : ℤ) : C t n = if n = 0 then t else 0 := by rw [← single_eq_C, Finsupp.single_apply]; aesop

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