Theorems · Theorem · group theory

Finset.sum_subtype

∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {p : ι → Prop} {F : Fintype (Subtype p)} (s : Finset ι),
  (∀ (x : ι), x ∈ s ↔ p x) → ∀ (f : ι → M), ∑ a ∈ s, f a = ∑ a, f ↑a

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

AddCommMonoid