coeff_def — Mathlib

English

If s is the finite support function with s() = n, then coeff(n) = MvPowerSeries.coeff(s).

Русский

Пусть s — функция с конечной опорой и s() = n; тогда coeff(n) = MvPowerSeries.coeff(s).

LaTeX

$$$ coeff\ (n)\ (R := R) = MvPowerSeries.coeff\ s $ при $ s() = n $$$

Lean4

theorem coeff_def {s : Unit →₀ ℕ} {n : ℕ} (h : s () = n) : coeff (R := R) n = MvPowerSeries.coeff s := by
  rw [coeff, ← h, ← Finsupp.unique_single s]

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