Commit 2021-12-24 23:09 d6ecc14a

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_multisetusing 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.