mathlib

d96e17df - feat(data/multiset/basic): add `map_le_map_iff` and `map_embedding` (#13082)

feat(data/multiset/basic): add `map_le_map_iff` and `map_embedding` (#13082) Adds lemmas `map_le_map_iff : s.map f ≤ t.map f ↔ s ≤ t` and `map_embedding : multiset α ↪o multiset β` for embedding `f`. Extracted from @huynhtrankhanh's #11162, moved here to a separate PR Co-authored-by: Huỳnh Trần Khanh [qcdz9r6wpcbh59@gmail.com](mailto:qcdz9r6wpcbh59@gmail.com)