mathlib3

8bb26a72 - chore(*): protect `to_fun` and `map_{add,zero,mul,one,div}` (#10580)

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.