Theorem: MvPolynomial.homogeneousComponent_eq_zero (DividedPowers/ForMathlib/Homogeneous.lean)

State before:
σ : Type u_1
τ : Type ?u.51956
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.51965
n : ℕ
φ ψ : MvPolynomial σ R
h : φ.totalDegree < n
⊢ (homogeneousComponent n) φ = 0
Tactic:
rw [totalDegree_eq_weightedTotalDegree] at h
State after:
σ : Type u_1
τ : Type ?u.51956
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.51965
n : ℕ
φ ψ : MvPolynomial σ R
h : weightedTotalDegree 1 φ < n
⊢ (homogeneousComponent n) φ = 0

State before:
σ : Type u_1
τ : Type ?u.51956
R : Type u_2
inst✝ : CommSemiring R
S : Type ?u.51965
n : ℕ
φ ψ : MvPolynomial σ R
h : weightedTotalDegree 1 φ < n
⊢ (homogeneousComponent n) φ = 0
Tactic:
exact weightedHomogeneousComponent_eq_zero n φ h
State after:
no goals