no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
P : Ideal R
hP : Ideal.IsPrime P
q : R[X]
c : (R ⧸ P)[X]
hq : map (mk P) q = c * X ^ n
hc0 : degree c = 0
⊢ ↑n = degree (map (mk P) q)
rw [hq, degree_mul, hc0, zero_add, degree_pow, degree_X, nsmul_one, Nat.cast_withBot]