Commit 2022-03-21 18:05 25ec622f

feat(data/polynomial/eval + data/polynomial/ring_division): move a lemma and remove assumptions (#12854) A lemma about composition of polynomials assumed comm_ring and is_domain. The new version assumes semiring. I golfed slightly the original proof: it may very well be that a shorter proof is available! I also moved the lemma, since it seems better for this lemma to appear in the file where the definition of comp appears.