Results about big operators with values in a field

theorem Multiset.sum_map_div {ι : Type u_1} {K : Type u_2} [DivisionSemiring K] (s : Multiset ι) (f : ι → K) (a : K) : (map (fun (x : ι) => f x / a) s).sum = (map f s).sum / a

theorem Finset.sum_div {ι : Type u_1} {K : Type u_2} [DivisionSemiring K] (s : Finset ι) (f : ι → K) (a : K) : (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a