coeff_monomial — Mathlib

English

For all m,n and a, coeff m (monomial n a) equals a if m=n, and 0 otherwise.

Русский

Для любых m,n и a: коэффициент m у мономa n a равен a, если m=n, иначе 0.

LaTeX

$$$\\mathrm{coeff}_m(\\mathrm{monomial}(n)\\, a) = \\begin{cases} a, & m=n \\\\ 0, & m\\neq n \\end{cases}$$$

Lean4

theorem coeff_monomial [DecidableEq σ] (m n : σ →₀ ℕ) (a : R) : coeff m (monomial n a) = if m = n then a else 0 :=
  by
  dsimp only [coeff, MvPowerSeries]
  rw [monomial_def, LinearMap.proj_apply (i := m), LinearMap.single_apply, Pi.single_apply]

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