mathlib3

6dcad021 - feat(linear_algebra/lagrange): Add recurrence formula for Lagrange polynomials (#11762)

feat(linear_algebra/lagrange): Add recurrence formula for Lagrange polynomials (#11762) I have also changed `interpolate` to take in a function `f : F → F` instead of `f : s → F`, since this makes the statement of the theorem nicer.