Commit 2023-03-09 14:54 60395bde

View on Github →

feat: port Data.Polynomial.Inductions (#2747)

Estimated changes

Modified Mathlib.lean

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

added theorem Polynomial.degree_lt_degree_mul_X

deleted theorem Polynomial.degree_lt_degree_mul_x

Created Mathlib/Data/Polynomial/Inductions.lean

added theorem Polynomial.coeff_divX

added theorem Polynomial.degree_divX_lt

added theorem Polynomial.degree_pos_induction_on

added def Polynomial.divX

added theorem Polynomial.divX_C

added theorem Polynomial.divX_add

added theorem Polynomial.divX_eq_zero_iff

added theorem Polynomial.divX_mul_X_add

added theorem Polynomial.natDegree_ne_zero_induction_on