R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ degree (↑C 1) ≤ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ degree 1 ≤ 0
rw [← C_1]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ degree (↑C 1) ≤ 0
exact degree_C_le