Commit 2020-07-20 12:54 65208ed7

View on Github →

refactor(data/polynomial/*): further refactors (#3435) There's a lot further to go, but I need to do other things for a while so will PR what I have so far.

Estimated changes

Modified src/data/polynomial/algebra_map.lean

Modified src/data/polynomial/basic.lean

added theorem polynomial.X_ne_zero

added theorem polynomial.coeff_X

added theorem polynomial.coeff_X_one

added theorem polynomial.coeff_X_zero

Modified src/data/polynomial/coeff.lean

added theorem polynomial.coeff_X_mul_zero

modified theorem polynomial.coeff_X_pow

added theorem polynomial.coeff_X_pow_self

modified theorem polynomial.coeff_mul_X_zero

Modified src/data/polynomial/degree.lean

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

Modified src/data/polynomial/derivative.lean

Modified src/data/polynomial/div.lean

Modified src/data/polynomial/eval.lean

Modified src/data/polynomial/field_division.lean

Modified src/data/polynomial/identities.lean

Modified src/data/polynomial/induction.lean

Modified src/data/polynomial/monic.lean

Modified src/data/polynomial/monomial.lean

deleted theorem polynomial.X_ne_zero

deleted theorem polynomial.coeff_X

deleted theorem polynomial.coeff_X_one

deleted theorem polynomial.coeff_X_zero

Modified src/data/polynomial/ring_division.lean