feat(data/mv_polynomial): API for mv polynomial.rename (#10921)
Relation between `rename` and `support`, `degrees` and `degree_of` when `f : σ → τ` is injective.
- I'm not sure if we already have something like `sup_map_multiset`.
- I've stated `sup_map_multiset`using `embedding` but I've used `injective` elsewhere because `mv_polynomial.rename` is written using `injective`.
- I'm not sure if we should have `map_domain_embedding_of_injective`.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
