Commit 2023-05-06 07:17 7482d3ea

View on Github →

feat: port LinearAlgebra.Lagrange (#3784)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Lagrange.lean

added theorem Lagrange.X_sub_C_dvd_nodal

added def Lagrange.basisDivisor

added theorem Lagrange.basisDivisor_add_symm

added theorem Lagrange.basisDivisor_eq_zero_iff

added theorem Lagrange.basisDivisor_inj

added theorem Lagrange.basisDivisor_ne_zero_iff

added theorem Lagrange.basisDivisor_self

added theorem Lagrange.basis_empty

added theorem Lagrange.basis_eq_prod_sub_inv_mul_nodal_div

added theorem Lagrange.basis_ne_zero

added theorem Lagrange.basis_pair_left

added theorem Lagrange.basis_pair_right

added theorem Lagrange.basis_singleton

added theorem Lagrange.degree_basis

added theorem Lagrange.degree_basisDivisor_of_ne

added theorem Lagrange.degree_basisDivisor_self

added theorem Lagrange.degree_interpolate_erase_lt

added theorem Lagrange.degree_interpolate_le

added theorem Lagrange.degree_interpolate_lt

added theorem Lagrange.degree_nodal

added theorem Lagrange.derivative_nodal

added theorem Lagrange.eq_interpolate

added theorem Lagrange.eq_interpolate_iff

added theorem Lagrange.eq_interpolate_of_eval_eq

added theorem Lagrange.eval_basisDivisor_left_of_ne

added theorem Lagrange.eval_basisDivisor_right

added theorem Lagrange.eval_basis_not_at_node

added theorem Lagrange.eval_basis_of_ne

added theorem Lagrange.eval_basis_self

added theorem Lagrange.eval_interpolate_at_node

added theorem Lagrange.eval_interpolate_not_at_node'

added theorem Lagrange.eval_interpolate_not_at_node

added theorem Lagrange.eval_nodal

added theorem Lagrange.eval_nodal_at_node

added theorem Lagrange.eval_nodal_derivative_eval_node_eq

added theorem Lagrange.eval_nodal_not_at_node

added def Lagrange.funEquivDegreeLT

added def Lagrange.interpolate

added theorem Lagrange.interpolate_empty

added theorem Lagrange.interpolate_eq_add_interpolate_erase

added theorem Lagrange.interpolate_eq_iff_values_eq_on

added theorem Lagrange.interpolate_eq_nodalWeight_mul_nodal_div_X_sub_C

added theorem Lagrange.interpolate_eq_of_values_eq_on

added theorem Lagrange.interpolate_eq_sum_interpolate_insert_sdiff

added theorem Lagrange.interpolate_one

added theorem Lagrange.interpolate_singleton

added theorem Lagrange.natDegree_basis

added theorem Lagrange.natDegree_basisDivisor_of_ne

added theorem Lagrange.natDegree_basisDivisor_self

added def Lagrange.nodal

added def Lagrange.nodalWeight

added theorem Lagrange.nodalWeight_eq_eval_nodal_derative

added theorem Lagrange.nodalWeight_eq_eval_nodal_erase_inv

added theorem Lagrange.nodalWeight_ne_zero

added theorem Lagrange.nodal_empty

added theorem Lagrange.nodal_eq

added theorem Lagrange.nodal_eq_mul_nodal_erase

added theorem Lagrange.nodal_erase_eq_nodal_div

added theorem Lagrange.nodal_insert_eq_nodal

added theorem Lagrange.sum_basis

added theorem Lagrange.sum_nodalWeight_mul_inv_sub_ne_zero

added theorem Lagrange.values_eq_on_of_interpolate_eq

added theorem Polynomial.eq_of_degree_sub_lt_of_eval_finset_eq

added theorem Polynomial.eq_of_degree_sub_lt_of_eval_index_eq

added theorem Polynomial.eq_of_degrees_lt_of_eval_finset_eq

added theorem Polynomial.eq_of_degrees_lt_of_eval_index_eq

added theorem Polynomial.eq_zero_of_degree_lt_of_eval_finset_eq_zero

added theorem Polynomial.eq_zero_of_degree_lt_of_eval_index_eq_zero