Commit 2020-08-13 12:59 2c4300b4

View on Github →

feat(data/polynomial): adds map_comp (#3736) Adds lemma saying that the map of the composition of two polynomials is the composition of the maps, as mentioned here.

Estimated changes

Modified src/algebra/big_operators/basic.lean

added theorem finset.prod_subset_one_on_sdiff

Modified src/data/polynomial/eval.lean

added theorem polynomial.map_comp

added theorem polynomial.map_sum

added theorem polynomial.support_map_subset