Commit 2022-02-04 02:03 6dcad021

View on Github →

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.

Estimated changes

Modified docs/undergrad.yaml

Modified src/linear_algebra/lagrange.lean

added theorem lagrange.basis_singleton_self

added theorem lagrange.degree_interpolate_erase

added theorem lagrange.eq_interpolate_of_eval_eq

modified theorem lagrange.eval_interpolate

added theorem lagrange.interpolate_eq_interpolate_erase_add

added theorem lagrange.interpolate_eq_of_eval_eq

added theorem lagrange.interpolate_singleton

modified def lagrange.linterpolate