no goals
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
⊢ IsWeightedHomogeneous w (↑(weightedHomogeneousComponent w n) φ) n
classical
intro d hd
contrapose! hd
rw [coeff_weightedHomogeneousComponent, if_neg hd]
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d (↑(weightedHomogeneousComponent w n) φ) ≠ 0
⊢ ↑(weightedDegree' w) d = n
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
⊢ IsWeightedHomogeneous w (↑(weightedHomogeneousComponent w n) φ) n
intro d hd
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ↑(weightedDegree' w) d ≠ n
⊢ coeff d (↑(weightedHomogeneousComponent w n) φ) = 0
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d (↑(weightedHomogeneousComponent w n) φ) ≠ 0
⊢ ↑(weightedDegree' w) d = n
contrapose! hd
no goals
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
n : M
φ ψ : MvPolynomial σ R
d : σ →₀ ℕ
hd : ↑(weightedDegree' w) d ≠ n
⊢ coeff d (↑(weightedHomogeneousComponent w n) φ) = 0
rw [coeff_weightedHomogeneousComponent, if_neg hd]