Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-02 21:22 e5befed7

View on Github →

chore(data/polynomial/degree): golf some proofs, add simple lemmas (#5185)

drop polynomial.nat_degree_C_mul_X_pow_of_nonzero; was a duplicate of polynomial.nat_degree_C_mul_X_pow;
golf the proof of nat_degree_C_mul_X_pow_le;
add more simp lemmas.

Estimated changes

Modified src/data/polynomial/degree/definitions.lean

added theorem polynomial.degree_mul_X

added theorem polynomial.degree_mul_X_pow

added theorem polynomial.degree_mul_monic

added theorem polynomial.leading_coeff_C_mul_X_pow

modified theorem polynomial.leading_coeff_X_pow

deleted theorem polynomial.leading_coeff_monomial'

modified theorem polynomial.leading_coeff_monomial

added theorem polynomial.leading_coeff_mul_X

modified theorem polynomial.leading_coeff_mul_X_pow

added theorem polynomial.leading_coeff_mul_monic

added theorem polynomial.monic_X_pow

added theorem polynomial.nat_degree_C_mul_X

deleted theorem polynomial.nat_degree_C_mul_X_pow_of_nonzero

Modified src/data/polynomial/div.lean