Commit 2021-12-03 14:32 8bb26a72
View on Github →chore(*): protect to_fun and map_{add,zero,mul,one,div} (#10580)
This PR prepares for #9888 by namespacing all usages of to_fun and map_{add,zero,mul,one,div} that do not involve the classes of #9888. This includes e.g. polynomial.map_add and multiset.map_add, which involve polynomial.map and multiset.map respectively.