F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ ∑ x in s, Lagrange.basis s v x = 1
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ ↑(interpolate s v) 1 = 1
simp_rw [interpolate_apply, Pi.one_apply, map_one, one_mul]
no goals
F : Type u_2
inst✝¹ : Field F
ι : Type u_1
inst✝ : DecidableEq ι
s t : Finset ι
i j : ι
v r r' : ι → F
hvs : Set.InjOn v ↑s
hs : Finset.Nonempty s
⊢ ∑ x in s, Lagrange.basis s v x = 1
exact sum_basis hvs hs