Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-28 07:50 005763ec

View on Github →

feat(linear_algebra/lagrange): Lagrange interpolation (#2764) Fixes #2600.

Estimated changes

Modified src/data/polynomial.lean

added theorem polynomial.degree_sub_le

Created src/linear_algebra/lagrange.lean

added def lagrange.basis

added theorem lagrange.basis_empty

added theorem lagrange.degree_interpolate_lt

added theorem lagrange.eq_interpolate

added theorem lagrange.eq_of_eval_eq

added theorem lagrange.eq_zero_of_eval_eq_zero

added theorem lagrange.eval_basis

added theorem lagrange.eval_basis_ne

added theorem lagrange.eval_basis_self

added theorem lagrange.eval_interpolate

added def lagrange.fun_equiv_degree_lt

added def lagrange.interpolate

added theorem lagrange.interpolate_add

added theorem lagrange.interpolate_empty

added theorem lagrange.interpolate_neg

added theorem lagrange.interpolate_smul

added theorem lagrange.interpolate_sub

added theorem lagrange.interpolate_zero

added def lagrange.linterpolate

added theorem lagrange.nat_degree_basis

Modified src/ring_theory/polynomial.lean

modified theorem polynomial.degree_le_mono

added def polynomial.degree_lt

added theorem polynomial.degree_lt_eq_span_X_pow

added theorem polynomial.degree_lt_mono

added theorem polynomial.mem_degree_lt