case h
σ : Type u_2
τ : Type ?u.5216
R : Type u_1
S : Type ?u.5222
inst✝ : CommSemiring R
n : ℕ
x✝ : MvPolynomial σ R
⊢ x✝ ∈ homogeneousSubmodule σ R n ↔ x✝ ∈ Finsupp.supported R R {d | ∑ i in d.support, ↑d i = n}
σ : Type u_2
τ : Type ?u.5216
R : Type u_1
S : Type ?u.5222
inst✝ : CommSemiring R
n : ℕ
⊢ homogeneousSubmodule σ R n = Finsupp.supported R R {d | ∑ i in d.support, ↑d i = n}
ext
case h
σ : Type u_2
τ : Type ?u.5216
R : Type u_1
S : Type ?u.5222
inst✝ : CommSemiring R
n : ℕ
x✝ : MvPolynomial σ R
⊢ x✝ ∈ homogeneousSubmodule σ R n ↔ ∀ (x : σ →₀ ℕ), x ∈ ↑x✝.support → x ∈ {d | ∑ i in d.support, ↑d i = n}
case h
σ : Type u_2
τ : Type ?u.5216
R : Type u_1
S : Type ?u.5222
inst✝ : CommSemiring R
n : ℕ
x✝ : MvPolynomial σ R
⊢ x✝ ∈ homogeneousSubmodule σ R n ↔ x✝ ∈ Finsupp.supported R R {d | ∑ i in d.support, ↑d i = n}
rw [Finsupp.mem_supported, Set.subset_def]
case h
σ : Type u_2
τ : Type ?u.5216
R : Type u_1
S : Type ?u.5222
inst✝ : CommSemiring R
n : ℕ
x✝ : MvPolynomial σ R
⊢ x✝ ∈ homogeneousSubmodule σ R n ↔ ∀ (x : σ →₀ ℕ), ↑x✝ x ≠ 0 → x ∈ {d | ∑ x in d.support, ↑d x = n}
case h
σ : Type u_2
τ : Type ?u.5216
R : Type u_1
S : Type ?u.5222
inst✝ : CommSemiring R
n : ℕ
x✝ : MvPolynomial σ R
⊢ x✝ ∈ homogeneousSubmodule σ R n ↔ ∀ (x : σ →₀ ℕ), x ∈ ↑x✝.support → x ∈ {d | ∑ i in d.support, ↑d i = n}
simp only [Finsupp.mem_support_iff, Finset.mem_coe]
no goals
case h
σ : Type u_2
τ : Type ?u.5216
R : Type u_1
S : Type ?u.5222
inst✝ : CommSemiring R
n : ℕ
x✝ : MvPolynomial σ R
⊢ x✝ ∈ homogeneousSubmodule σ R n ↔ ∀ (x : σ →₀ ℕ), ↑x✝ x ≠ 0 → x ∈ {d | ∑ x in d.support, ↑d x = n}
rfl