R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (∀ (m : ℕ), m < 1 → ↑(coeff R m) φ = 0) ↔ ↑(coeff R 0) φ = 0
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ X ∣ φ ↔ ↑(constantCoeff R) φ = 0
rw [← pow_one (X : PowerSeries R), X_pow_dvd_iff, ← coeff_zero_eq_constantCoeff_apply]
case mp
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : ∀ (m : ℕ), m < 1 → ↑(coeff R m) φ = 0
⊢ ↑(coeff R 0) φ = 0

case mpr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : ↑(coeff R 0) φ = 0
⊢ ∀ (m : ℕ), m < 1 → ↑(coeff R m) φ = 0
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
⊢ (∀ (m : ℕ), m < 1 → ↑(coeff R m) φ = 0) ↔ ↑(coeff R 0) φ = 0
constructor <;> intro h
no goals
case mp
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : ∀ (m : ℕ), m < 1 → ↑(coeff R m) φ = 0
⊢ ↑(coeff R 0) φ = 0
exact h 0 zero_lt_one
case mpr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : ↑(coeff R 0) φ = 0
m : ℕ
hm : m < 1
⊢ ↑(coeff R m) φ = 0
case mpr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : ↑(coeff R 0) φ = 0
⊢ ∀ (m : ℕ), m < 1 → ↑(coeff R m) φ = 0
intro m hm
no goals
case mpr
R : Type u_1
inst✝ : Semiring R
φ : PowerSeries R
h : ↑(coeff R 0) φ = 0
m : ℕ
hm : m < 1
⊢ ↑(coeff R m) φ = 0
rwa [Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hm)]