Commit 2020-08-20 11:47 46310185

View on Github →

feat(data/polynomial): Add polynomial/eval lemmas (#3876) Add some lemmas about polynomial. In particular, add lemmas about eval2 for the case that the ring S that we evaluate into is non-commutative.

Estimated changes

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

added theorem polynomial.leading_coeff_X_add_C

Modified src/data/polynomial/eval.lean

added theorem polynomial.eval₂_endomorphism_algebra_map

added theorem polynomial.eval₂_list_prod_noncomm

added theorem polynomial.eval₂_mul_noncomm

added def polynomial.eval₂_ring_hom_noncomm

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.units_coeff_zero_smul