mathlib

25ec622f - feat(data/polynomial/eval + data/polynomial/ring_division): move a lemma and remove assumptions (#12854)

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.