Commit 2021-10-08 14:22 745cbfc6

feat(data/polynomial): %ₘ as a linear map (#9532) This PR bundles (%ₘ) = polynomial.mod_by_monic into a linear map. In a follow-up PR, I'll show this map descends to a linear map adjoin_root q → polynomial R, thereby (computably) assigning coefficients to each element in adjoin_root q.