σ : Type u
R : Type v
inst✝¹ : CommRing R
p✝ m : ℕ
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ (∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n) ↔ ∀ (i : σ) (b : σ →₀ ℕ), b ∈ support p → ↑b i ≤ n
σ : Type u
R : Type v
inst✝¹ : CommRing R
p✝ m : ℕ
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ p ∈ restrictDegree σ R n ↔ ∀ (i : σ), Multiset.count i (degrees p) ≤ n
simp only [mem_restrictDegree, degrees_def, Multiset.count_finset_sup, Finsupp.count_toMultiset,
  Finset.sup_le_iff]
no goals
σ : Type u
R : Type v
inst✝¹ : CommRing R
p✝ m : ℕ
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ (∀ (s : σ →₀ ℕ), s ∈ support p → ∀ (i : σ), ↑s i ≤ n) ↔ ∀ (i : σ) (b : σ →₀ ℕ), b ∈ support p → ↑b i ≤ n
exact ⟨fun h n s hs => h s hs n, fun h s hs n => h n s hs⟩