coeff_X — Mathlib

English

Let n be a finitely supported function n : σ → ℕ and s ∈ σ. Then the coefficient of X_s at index n is 1 if n equals single s 1, and 0 otherwise.

Русский

Пусть n : σ → ℕ имеет конечную опору, и пусть s ∈ σ. Тогда коэффициент X_s на позиции n равен 1, если n = single(s,1), иначе 0.

LaTeX

$$$\operatorname{coeff} (n) (X_s) = \begin{cases} 1, & n = \mathrm{single}(s,1) \\\\ 0, & \text{otherwise} \end{cases}$$$

Lean4

theorem coeff_X [DecidableEq σ] (n : σ →₀ ℕ) (s : σ) :
    coeff n (X s : MvPowerSeries σ R) = if n = single s 1 then 1 else 0 :=
  coeff_monomial _ _ _

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