eq_zero_iff_forall_coeff_eq_zero_and

Mathlib.RingTheory.MvPowerSeries.Order

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.eq_zero_iff_forall_coeff_eq_zero_and

English

A mv_power_series is zero iff all its coefficients are zero.

Русский

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

LaTeX

$$f = 0 ↔ (∀ d, coeff d f = 0)$$

Lean4

theorem eq_zero_iff_forall_coeff_eq_zero_and : f = 0 ↔ (∀ d : σ →₀ ℕ, coeff d f = 0) :=
  MvPowerSeries.ext_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru