R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (¬∃ n, ↑(coeff R n) φ ≠ 0) ↔ ¬φ ≠ 0
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (∃ n, ↑(coeff R n) φ ≠ 0) ↔ φ ≠ 0
refine' not_iff_not.mp _
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (∀ (n : ℕ), ↑(coeff R n) φ = 0) ↔ φ = 0
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (¬∃ n, ↑(coeff R n) φ ≠ 0) ↔ ¬φ ≠ 0
push_neg
no goals
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (∀ (n : ℕ), ↑(coeff R n) φ = 0) ↔ φ = 0
simp [PowerSeries.ext_iff]