case a
σ : Type u_1
τ : Type ?u.360896
R : Type u_2
S : Type ?u.360902
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i in range (totalDegree φ + 1), ↑(homogeneousComponent i) φ) = coeff d φ
σ : Type u_1
τ : Type ?u.360896
R : Type u_2
S : Type ?u.360902
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ ∑ i in range (totalDegree φ + 1), ↑(homogeneousComponent i) φ = φ
ext1 d
case a
σ : Type u_1
τ : Type ?u.360896
R : Type u_2
S : Type ?u.360902
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ totalDegree φ < Finset.sum d.support ↑d → 0 = coeff d φ
case a
σ : Type u_1
τ : Type ?u.360896
R : Type u_2
S : Type ?u.360902
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i in range (totalDegree φ + 1), ↑(homogeneousComponent i) φ) = coeff d φ
suffices φ.totalDegree < d.support.sum d → 0 = coeff d φ by
  simpa [coeff_sum, coeff_homogeneousComponent]
no goals
case a
σ : Type u_1
τ : Type ?u.360896
R : Type u_2
S : Type ?u.360902
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ totalDegree φ < Finset.sum d.support ↑d → 0 = coeff d φ
exact fun h => (coeff_eq_zero_of_totalDegree_lt h).symm
no goals
σ : Type u_1
τ : Type ?u.360896
R : Type u_2
S : Type ?u.360902
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
this : totalDegree φ < Finset.sum d.support ↑d → 0 = coeff d φ
⊢ coeff d (∑ i in range (totalDegree φ + 1), ↑(homogeneousComponent i) φ) = coeff d φ
simpa [coeff_sum, coeff_homogeneousComponent]