Commit 2023-08-21 01:30 c6e395dd

View on Github →

feat: add theorem about nodal on Subgroup (#6495) A lemma about the vanishing polynomial.

Estimated changes

Modified Mathlib/Data/Polynomial/Degree/Definitions.lean

added theorem Polynomial.leadingCoeff_add_of_degree_lt'

added theorem Polynomial.leadingCoeff_sub_of_degree_eq

added theorem Polynomial.leadingCoeff_sub_of_degree_lt'

added theorem Polynomial.leadingCoeff_sub_of_degree_lt

Modified Mathlib/LinearAlgebra/Lagrange.lean

added theorem Lagrange.nodal_monic

added theorem Lagrange.nodal_subgroup_eq_X_pow_card_sub_one

added theorem Polynomial.eq_of_degree_le_of_eval_finset_eq

added theorem Polynomial.eq_of_degree_le_of_eval_index_eq