no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i j : ι
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ degree (Lagrange.basis s v i) = ↑(card s - 1)
rw [degree_eq_natDegree (basis_ne_zero hvs hi), natDegree_basis hvs hi]