Commit 2023-09-14 07:53 48d20bd1

View on Github →

feat: expand API for Polynomial.divX and some related results (#6428) Various lemmas about Polynomial.natDegree

Estimated changes

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

added theorem Polynomial.eq_one_of_monic_natDegree_zero

Modified Mathlib/Data/Polynomial/Div.lean

added theorem Polynomial.X_dvd_sub_C

added theorem Polynomial.natDegree_modByMonic_le

Modified Mathlib/Data/Polynomial/Inductions.lean

added theorem Polynomial.X_mul_divX_add

added theorem Polynomial.divX_C_mul

added theorem Polynomial.divX_C_mul_X_pow

added theorem Polynomial.divX_X_pow

added def Polynomial.divX_hom

added theorem Polynomial.divX_hom_toFun

added theorem Polynomial.divX_one

added theorem Polynomial.divX_zero

added theorem Polynomial.natDegree_divX_eq_natDegree_tsub_one

added theorem Polynomial.natDegree_divX_le