Results about big operators with values in a field #
theorem
Finset.sum_div
{ι : Type u_1}
{K : Type u_2}
[DivisionSemiring K]
(s : Finset ι)
(f : ι → K)
(a : K)
:
@[simp]
theorem
Finset.dens_disjiUnion
{α : Type u_3}
{β : Type u_4}
[Fintype β]
(s : Finset α)
(t : α → Finset β)
(h : (↑s).PairwiseDisjoint t)
:
theorem
Finset.dens_biUnion
{α : Type u_3}
{β : Type u_4}
[Fintype β]
{s : Finset α}
{t : α → Finset β}
[DecidableEq β]
(h : (↑s).PairwiseDisjoint t)
:
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)
: