English
For any indices s, s' and natural numbers n, n', the coefficient of X_s^n at the exponent Finsupp.single s' n' equals 1 precisely when either (s = s' and n = n') or (n = 0 and n' = 0); otherwise it is 0.
Русский
Для любых индексов s, s' и натуральных чисел n, n' коэффициент X_s^n при экспоненте Finsupp.single s' n' равен 1 тогда и только тогда, когда либо (s = s' и n = n'), либо (n = 0 и n' = 0); в противном случае равен 0.
LaTeX
$$$(X (R := R)\\, s^n).coeff\\bigl(Finsupp.single s' n'\\bigr) = \\begin{cases}1 & \\text{если } s = s' \\wedge n = n' \\\\ & \\text{или } n = 0 \\wedge n' = 0, \\\\ 0 & \\text{иначе} \\end{cases}$$$
Lean4
theorem coeff_single_X_pow [DecidableEq σ] (s s' : σ) (n n' : ℕ) :
(X (R := R) s ^ n).coeff (Finsupp.single s' n') = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0 := by
simp only [coeff_X_pow, single_eq_single_iff]
