ne_zero_iff_exists_coeff_ne_zero — Mathlib

English

A power series f is nonzero if and only if there exists a coefficient that is nonzero.

Русский

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

LaTeX

$$$f \\neq 0 \\iff \\exists d : \\sigma \\to_0 \\mathbb{N}, \\mathrm{coeff}_d f \\neq 0$$$

Lean4

theorem ne_zero_iff_exists_coeff_ne_zero (f : MvPowerSeries σ R) : f ≠ 0 ↔ (∃ d : σ →₀ ℕ, coeff d f ≠ 0) := by
  simp only [MvPowerSeries.ext_iff, ne_eq, coeff_zero, not_forall]

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