Commit 2023-09-07 00:04 bf8d6d9e

View on Github →

feat(LinearAlgebra/Lagrange): Generalize typeclasses. (#6714) Generalize some key definitions in the definition of Lagrange interpolation. In particular, the definition of the nodal polynomial does not need to be over a field.

Estimated changes

Modified Mathlib/LinearAlgebra/Lagrange.lean

modified theorem Lagrange.X_sub_C_dvd_nodal

modified theorem Lagrange.degree_nodal

modified theorem Lagrange.derivative_nodal

modified theorem Lagrange.eval_nodal

modified theorem Lagrange.eval_nodal_at_node

modified theorem Lagrange.eval_nodal_derivative_eval_node_eq

modified theorem Lagrange.eval_nodal_not_at_node

added theorem Lagrange.natDegree_nodal

modified def Lagrange.nodal

modified theorem Lagrange.nodal_eq

modified theorem Lagrange.nodal_eq_mul_nodal_erase

modified theorem Lagrange.nodal_insert_eq_nodal

added theorem Lagrange.nodal_ne_zero

modified theorem Lagrange.nodal_subgroup_eq_X_pow_card_sub_one