Commit 2020-06-30 05:20 da481e77

View on Github →

chore(data/polynomial): partial move from is_ring_hom to ring_hom (#3213) This does not attempt to do a complete refactor of polynomial.lean and mv_polynomial.lean to remove use of is_ring_hom, but only to fix eval₂ which we need for the current work on Cayley-Hamilton. Having struggled with these two files for the last few days, I'm keen to get them cleaned up, so I'll promise to return to this more thoroughly in a later PR.

Estimated changes

Modified src/data/mv_polynomial.lean

modified def mv_polynomial.C

Modified src/data/polynomial.lean

modified def polynomial.eval

added theorem polynomial.eval₂_X_pow

modified theorem polynomial.eval₂_comp

modified theorem polynomial.eval₂_hom

modified theorem polynomial.eval₂_map

added theorem polynomial.eval₂_monomial

modified theorem polynomial.eval₂_neg

modified theorem polynomial.eval₂_pow

modified theorem polynomial.eval₂_sub

modified theorem polynomial.hom_eval₂

modified def polynomial.map

Modified src/ring_theory/localization.lean

Modified src/ring_theory/polynomial.lean