coeff_monomial — Mathlib

English

The nth coefficient of the monomial with index n and value a is a, and it is 0 otherwise.

Русский

Коэффициент n монома с индексом n и значением a равен a, а при других индексах коэффициент равен 0.

LaTeX

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

Lean4

theorem coeff_monomial (m n : ℕ) (a : R) : coeff m (monomial n a) = if m = n then a else 0 :=
  calc
    coeff m (monomial n a) = _ := MvPowerSeries.coeff_monomial _ _ _
    _ = if m = n then a else 0 := by simp only [Finsupp.unique_single_eq_iff]

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