Multiset min/max

Stream: Is there code for X?

[Hubert Ostoja-Petkowski]

Finset has min and max and various useful theorems about them defined, however for multiset I can only find max_le_of_forall_le and max_nat_le_of_forall_le. I've been writing ((multiset.range n).map (λ k, |s k|)).fold max 0 as the max of the abs of the first n elements of a sequence, is there some duplicate-erasing version of map I could use to access the finset min/max theorems?

[Yaël Dillies]

docs#multiset.to_finset ?