Commit 2020-07-19 05:43 8312419c

View on Github →

refactor(data/polynomial): remove has_coe_to_fun, and @[reducible] on monomial (#3420) I'm going to refactor in stages, trying to clean up some of the cruftier aspects of data/polynomial/*. This PR:

removes the has_coe_to_fun on polynomial

Estimated changes

Modified src/data/polynomial/basic.lean

deleted theorem polynomial.apply_eq_coeff

deleted def polynomial.coeff_coe_to_fun

added theorem polynomial.coeff_monomial

modified theorem polynomial.coeff_one_zero

added theorem polynomial.monomial_mul_monomial

Modified src/data/polynomial/coeff.lean

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

Modified src/data/polynomial/derivative.lean

Modified src/data/polynomial/div.lean

added theorem polynomial.apply_eq_coeff

added def polynomial.coeff_coe_to_fun

Modified src/data/polynomial/eval.lean

Modified src/data/polynomial/monomial.lean

modified theorem polynomial.coeff_C_zero

modified theorem polynomial.coeff_X

modified theorem polynomial.coeff_X_one

modified theorem polynomial.coeff_X_zero

Modified src/ring_theory/polynomial_algebra.lean