Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-11 11:37 45787967

View on Github →

feat(data/polynomial): various lemmas about degree and monic and coeff

Estimated changes

Modified data/polynomial.lean

modified theorem polynomial.coeff_X

modified theorem polynomial.coeff_add

modified theorem polynomial.coeff_neg

added theorem polynomial.coeff_sub

added theorem polynomial.degree_C_mul_X_pow_le

added theorem polynomial.degree_X_le

added theorem polynomial.degree_X_pow_le

added theorem polynomial.degree_le_iff_coeff_zero

added theorem polynomial.degree_mod_by_monic_le

added theorem polynomial.leading_coeff_mul_X_pow

added theorem polynomial.monic_X_add_C

added theorem polynomial.monic_X_pow_add

added theorem polynomial.monic_X_pow_sub

modified theorem polynomial.monic_X_sub_C

added theorem polynomial.monic_of_degree_le

added theorem polynomial.nat_degree_le_of_degree_le