Theorems · Theorem · combinatorics

Fin.sum_uIcc_castAdd

∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∑ i ∈ Finset.uIcc (Fin.castAdd m a) (Fin.castAdd m b), f i = ∑ i ∈ Finset.uIcc a b, f (Fin.castAdd m i)

Defined in

Mathlib.Algebra.BigOperators.Fin

Cited by

0 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoid