coeff_X' — Mathlib

English

Coefficient of X_i equals 1 when m equals δ_i, and 0 otherwise, i.e., coeff m (X_i) = 1 if m = single i 1, else 0.

Русский

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

LaTeX

$$[DecidableEq σ] (i) (m) : \mathrm{coeff}\ m (X_i) = \text{if }(\mathrm{Finsupp.single}\ i\ 1)=m\ then\ 1\ else\ 0$$

Lean4

theorem coeff_X' [DecidableEq σ] (i : σ) (m) :
    coeff m (X i : MvPolynomial σ R) = if Finsupp.single i 1 = m then 1 else 0 := by rw [← coeff_X_pow, pow_one]

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