σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), ↑m s < 1 → ↑(coeff R m) φ = 0) ↔ ∀ (m : σ →₀ ℕ), ↑m s = 0 → ↑(coeff R m) φ = 0
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), ↑m s = 0 → ↑(coeff R m) φ = 0
rw [← pow_one (X s : MvPowerSeries σ R), X_pow_dvd_iff]
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < 1 → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
hm : ↑m s = 0
⊢ ↑(coeff R m) φ = 0

case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s = 0 → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
hm : ↑m s < 1
⊢ ↑(coeff R m) φ = 0
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ), ↑m s < 1 → ↑(coeff R m) φ = 0) ↔ ∀ (m : σ →₀ ℕ), ↑m s = 0 → ↑(coeff R m) φ = 0
constructor <;> intro h m hm
no goals
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s < 1 → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
hm : ↑m s = 0
⊢ ↑(coeff R m) φ = 0
exact h m (hm.symm ▸ zero_lt_one)
no goals
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), ↑m s = 0 → ↑(coeff R m) φ = 0
m : σ →₀ ℕ
hm : ↑m s < 1
⊢ ↑(coeff R m) φ = 0
exact h m (Nat.eq_zero_of_le_zero <| Nat.le_of_succ_le_succ hm)