R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ degree (↑(monomial n) a) ≤ ↑n
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ degree (↑C a * X ^ n) ≤ ↑n
rw [C_mul_X_pow_eq_monomial]
no goals
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ degree (↑(monomial n) a) ≤ ↑n
apply degree_monomial_le