coeff_X_pow — Mathlib

English

The coefficient of m in X_i^k is 1 if m equals δ_i^k and 0 otherwise.

Русский

Коэффициент при m в X_i^k равен 1, если m совпадает с δ_i^k, иначе 0.

LaTeX

$$$\mathrm{coeff}\ m (X_i^k) = \text{if } \mathrm{Finsupp.single}\ i\ k = m \text{ then } 1 \text{ else } 0$$$

Lean4

theorem coeff_X_pow [DecidableEq σ] (i : σ) (m) (k : ℕ) :
    coeff m (X i ^ k : MvPolynomial σ R) = if Finsupp.single i k = m then 1 else 0 :=
  by
  have := coeff_monomial m (Finsupp.single i k) (1 : R)
  rwa [@monomial_eq _ _ (1 : R) (Finsupp.single i k) _, C_1, one_mul, Finsupp.prod_single_index] at this
  exact pow_zero _

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