coeff_X_pow — Mathlib

English

For any m : σ →₀ ℕ, s ∈ σ, n ∈ ℕ, the coefficient of (X_s)^n at m is 1 if m = single s n, otherwise 0.

Русский

Для любого m : σ → ℕ , s ∈ σ, n ∈ ℕ коэффициент (X_s)^n на позиции m равен 1, если m = single s n, иначе 0.

LaTeX

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

Lean4

theorem coeff_X_pow [DecidableEq σ] (m : σ →₀ ℕ) (s : σ) (n : ℕ) :
    coeff m ((X s : MvPowerSeries σ R) ^ n) = if m = single s n then 1 else 0 := by rw [X_pow_eq s n, coeff_monomial]

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