no goals
F : Type u_1
inst✝ : Field F
ι : Type u_2
s : Finset ι
v : ι → F
i : ι
r : ι → F
x : F
⊢ degree (nodal s v) = ↑(card s)
simp_rw [nodal, degree_prod, degree_X_sub_C, sum_const, Nat.smul_one_eq_coe]