R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ degree (↑C a * T 0) = 0
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ degree (↑C a) = 0
rw [← mul_one (C a), ← T_zero]
no goals
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ degree (↑C a * T 0) = 0
exact degree_C_mul_T 0 a a0