multiset equivalent of is_absolute_value.abv_sum

Stream: Is there code for X?

[Xavier Roblot]

I am looking for the multiset equivalent of docs#is_absolute_value.abv_sum. Something like:

lemma multiset.is_absolute_value.abv_sum {ι : Type*} {S : Type*} {T : Type*} [semiring T]
  [ordered_semiring S] (abv : T → S) [is_absolute_value abv] (f : ι → T) (s : multiset ι) :
  abv (multiset.map f s).sum ≤ (multiset.map (abv ∘ f) s).sum :=
begin
  sorry,
end

It would be also convenient for me to have an equivalent of docs#is_absolute_value.map_prod:

lemma multiset.is_absolute_value.abv.map_prod {ι : Type*} {S : Type*} {T : Type*}
  [comm_semiring T] [comm_semiring S] [ordered_semiring S] (abv : T → S) [is_absolute_value abv]
  (s : multiset ι) (f : ι → T) :
  abv (multiset.map f s).prod = (multiset.map (abv ∘ f) s).prod :=
begin
  sorry,
end

I should be able to prove these but I thought they might exist already or maybe there is an easy way to deduce them from the finset versions that I don't know about

[Riccardo Brasca]

If you have a normed space these results can be there for the norm (but I didn't check)

[Xavier Roblot]

That's a good idea, but I don't think it's there. I guess I'll just do my own versions