Mathlib Map

Theorems · Theorem · combinatorics

Fin.sum_univ_add

∀ {M : Type u_2} [inst : AddCommMonoid M] {a b : ℕ} (f : Fin (a + b) → M),
  ∑ i, f i = ∑ i, f (Fin.castAdd b i) + ∑ i, f (Fin.natAdd a i)
Defined in
Mathlib.Algebra.BigOperators.Fin
Cited by
2 results in Mathlib
Foundations
Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
AddCommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

TensorProduct.exists_sum_tmul_eq · cited by 2TensorProduct.exists_sum_…Fin.sum_trunc · cited by 1Fin.sum_truncAddCommMonoid · cited by 12281AddCommMonoidFinset.sum · cited by 5195Finset.sumEquiv.symm · cited by 3681Equiv.symmFinset.univ · cited by 3473Finset.univEquiv.apply_symm_apply · cited by 346Equiv.apply_symm_applyEquiv.toFun · cited by 279Equiv.toFunFintype.sum_equiv · cited by 35Fintype.sum_equivfinSumFinEquiv · cited by 33finSumFinEquivFintype.sum_sum_type · cited by 22Fintype.sum_sum_typeFin.sum_univ_addCITED BYCITES

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.