σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ ∀ (b : σ →₀ ℕ), b ∈ support p → (Finsupp.sum b fun x e => e) ≤ m
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ totalDegree p ≤ m
rw [totalDegree, Finset.sup_le_iff]
no goals
σ : Type u
R : Type v
inst✝ : CommRing R
p✝ m : ℕ
p : MvPolynomial σ R
⊢ p ∈ restrictTotalDegree σ R m ↔ ∀ (b : σ →₀ ℕ), b ∈ support p → (Finsupp.sum b fun x e => e) ≤ m
rfl