eq_zero_iff_forall_coeff_zero — Mathlib

English

A multivariate power series f is zero if and only if all its coefficients are zero.

Русский

Многовекторная формальная серия f равна нулю тогда и только тогда, когда все её коэффициенты равны нулю.

LaTeX

$$$f = 0 \\iff (\\forall d : \\sigma \\to_0 \\mathbb{N}, \\mathrm{coeff}_d f = 0)$$$

Lean4

theorem eq_zero_iff_forall_coeff_zero {f : MvPowerSeries σ R} : f = 0 ↔ (∀ d : σ →₀ ℕ, coeff d f = 0) :=
  MvPowerSeries.ext_iff

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