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

@[simp]

theorem Finset.dens_disjiUnion {α : Type u_3} {β : Type u_4} [Fintype β] (s : Finset α) (t : α → Finset β) (h : (↑s).PairwiseDisjoint t) : (s.disjiUnion t h).dens = ∑ a ∈ s, (t a).dens

theorem Finset.dens_biUnion {α : Type u_3} {β : Type u_4} [Fintype β] {s : Finset α} {t : α → Finset β} [DecidableEq β] (h : (↑s).PairwiseDisjoint t) : (s.biUnion t).dens = ∑ u ∈ s, (t u).dens

theorem Finset.dens_biUnion_le {α : Type u_3} {β : Type u_4} [Fintype β] {s : Finset α} {t : α → Finset β} [DecidableEq β] : (s.biUnion t).dens ≤ ∑ a ∈ s, (t a).dens

theorem Finset.dens_eq_sum_dens_fiberwise {α : Type u_3} {β : Type u_4} [Fintype β] {s : Finset α} [DecidableEq α] {f : β → α} {t : Finset β} (h : Set.MapsTo f ↑t ↑s) : t.dens = ∑ a ∈ s, {b ∈ t | f b = a}.dens

theorem Finset.dens_eq_sum_dens_image {α : Type u_3} {β : Type u_4} [Fintype β] [DecidableEq α] (f : β → α) (t : Finset β) : t.dens = ∑ a ∈ image f t, {b ∈ t | f b = a}.dens