R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ card (support p) ≤ card (range (natDegree p + 1))
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ card (support p) ≤ natDegree p + 1
rw [← Finset.card_range (p.natDegree + 1)]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ card (support p) ≤ card (range (natDegree p + 1))
exact Finset.card_le_of_subset supp_subset_range_natDegree_succ