∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {M : Type u_2} [inst_2 : AddCommMonoid M]
  (f : AbsoluteValue K ℝ → M), (Multiset.map f Height.AdmissibleAbsValues.archAbsVal).sum = ∑ v, v.mult • f ↑v