mathlib

1563242e - feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. (#15036)

feat(linear_algebra/lagrange): Refactor lagrange interpolation and add extended proofs. (#15036) The current formulation of Lagrange interpolants phrases things in terms of a finset of nodes, and functions interpolated at those nodes. This changes things in order to allow for indexed nodes and weights. It also extends various functionalities of the lagrange interpolation. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>