R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ degree (↑C 1 * T n) = ↑n
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ degree (T n) = ↑n
rw [← one_mul (T n), ← map_one C]
no goals
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ degree (↑C 1 * T n) = ↑n
exact degree_C_mul_T n 1 (one_ne_zero : (1 : R) ≠ 0)