Documentation

Mathlib.Algebra.BigOperators.Field

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) :
(∑ is, f i) / a = is, 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 = as, (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 = us, (t u).dens
theorem Finset.dens_biUnion_le {α : Type u_3} {β : Type u_4} [Fintype β] {s : Finset α} {t : αFinset β} [DecidableEq β] :
(s.biUnion t).dens as, (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 = as, {bt | f b = a}.dens
theorem Finset.dens_eq_sum_dens_image {α : Type u_3} {β : Type u_4} [Fintype β] [DecidableEq α] (f : βα) (t : Finset β) :
t.dens = aimage f t, {bt | f b = a}.dens