σ : Type u_1
τ : Type ?u.181825
R : Type u_2
S : Type ?u.181831
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d (↑(homogeneousComponent n) φ) ≠ 0
⊢ ∑ i in d.support, ↑d i = n
σ : Type u_1
τ : Type ?u.181825
R : Type u_2
S : Type ?u.181831
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
⊢ IsHomogeneous (↑(homogeneousComponent n) φ) n
intro d hd
σ : Type u_1
τ : Type ?u.181825
R : Type u_2
S : Type ?u.181831
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ∑ x in d.support, ↑d x ≠ n
⊢ coeff d (↑(homogeneousComponent n) φ) = 0
σ : Type u_1
τ : Type ?u.181825
R : Type u_2
S : Type ?u.181831
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d (↑(homogeneousComponent n) φ) ≠ 0
⊢ ∑ i in d.support, ↑d i = n
contrapose! hd
no goals
σ : Type u_1
τ : Type ?u.181825
R : Type u_2
S : Type ?u.181831
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ∑ x in d.support, ↑d x ≠ n
⊢ coeff d (↑(homogeneousComponent n) φ) = 0
rw [coeff_homogeneousComponent, if_neg hd]