ext x
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
⊢ ((homogeneousComponent n) p).support = filter (fun d => (d.sum fun x m => m) = n) p.support
case a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial ι R
x : ι →₀ ℕ
⊢ x ∈ ((homogeneousComponent n) p).support ↔ x ∈ filter (fun d => (d.sum fun x m => m) = n) p.support