coeff_single_X — Mathlib

English

Let s and s' be indices in σ and n a natural number. The coefficient of X_s at the exponent Finsupp.single s' n equals 1 if n = 1 and s = s', and 0 otherwise.

Русский

Пусть s, s' — индексы в σ, и n — натуральное число. Коэффициент X_s при экспоненте Finsupp.single s' n равен 1, если n = 1 и s = s', иначе 0.

LaTeX

$$$(X s).coeff\\bigl(Finsupp.single s' n\\bigr) = \\begin{cases}1 & \\text{если } n = 1 \\wedge s = s' \\\\ 0 & \\text{иначе} \\end{cases}$$$

Lean4

@[simp]
theorem coeff_single_X [DecidableEq σ] (s s' : σ) (n : ℕ) :
    (X s).coeff (R := R) (Finsupp.single s' n) = if n = 1 ∧ s = s' then 1 else 0 := by
  simpa [eq_comm, and_comm] using coeff_single_X_pow s s' 1 n

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