Commit 2020-07-14 15:06 f7825bf5

View on Github →

feat(algebra/polynomial): big_operators lemmas for polynomials (#3378) This starts a new folder algebra/polynomial. As we refactor data/polynomial.lean, much of that content should land in this folder.

Estimated changes

Created src/algebra/polynomial/basic.lean

added theorem polynomial.coe_aeval_eq_eval

added theorem polynomial.coeff_zero_eq_aeval_zero

added def polynomial.leading_coeff_hom

added theorem polynomial.leading_coeff_hom_apply

Created src/algebra/polynomial/big_operators.lean

added theorem polynomial.leading_coeff_prod'

added theorem polynomial.leading_coeff_prod

added theorem polynomial.monic_prod_of_monic

added theorem polynomial.nat_degree_prod_eq'

added theorem polynomial.nat_degree_prod_eq

added theorem polynomial.nat_degree_prod_eq_of_monic

added theorem polynomial.nat_degree_prod_le