no goals
σ : Type u_1
R : Type ?u.1713985
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
h : φ⁻¹ = 0
⊢ ↑(constantCoeff σ k) φ = 0
simpa using congr_arg (constantCoeff σ k) h
σ : Type u_1
R : Type ?u.1713985
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
h : ↑(constantCoeff σ k) φ = 0
n : σ →₀ ℕ
⊢ (if n = 0 then (↑(constantCoeff σ k) φ)⁻¹
    else
      -(↑(constantCoeff σ k) φ)⁻¹ *
        ∑ x in antidiagonal n, if x.snd < n then ↑(coeff k x.fst) φ * ↑(coeff k x.snd) φ⁻¹ else 0) =
    ↑(coeff k n) 0
σ : Type u_1
R : Type ?u.1713985
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
h : ↑(constantCoeff σ k) φ = 0
n : σ →₀ ℕ
⊢ ↑(coeff k n) φ⁻¹ = ↑(coeff k n) 0
rw [coeff_inv]
no goals
σ : Type u_1
R : Type ?u.1713985
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
h : ↑(constantCoeff σ k) φ = 0
n : σ →₀ ℕ
⊢ (if n = 0 then (↑(constantCoeff σ k) φ)⁻¹
    else
      -(↑(constantCoeff σ k) φ)⁻¹ *
        ∑ x in antidiagonal n, if x.snd < n then ↑(coeff k x.fst) φ * ↑(coeff k x.snd) φ⁻¹ else 0) =
    ↑(coeff k n) 0
split_ifs <;>
  simp only [h, map_zero, zero_mul, inv_zero, neg_zero]