forall_coeff_eq_zero — Mathlib

English

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

Русский

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

LaTeX

$$$$(\forall n \in \mathbb{N}, \operatorname{coeff}_n(\phi) = 0) \iff \phi = 0$$$$

Lean4

@[simp]
theorem forall_coeff_eq_zero (φ : R⟦X⟧) : (∀ n, coeff n φ = 0) ↔ φ = 0 :=
  ⟨fun h => ext h, fun h => by simp [h]⟩

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