σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
n : ℕ
⊢ ↑p.support ⊆ {n_1 | ∀ (i : σ), ↑n_1 i ≤ n} ↔ ∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
n : ℕ
⊢ p ∈ restrictDegree σ R n ↔ ∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n
rw [restrictDegree, Finsupp.mem_supported]
no goals
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
n : ℕ
⊢ ↑p.support ⊆ {n_1 | ∀ (i : σ), ↑n_1 i ≤ n} ↔ ∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n
rfl