Theorems · Theorem · general algebraic systems

Finsupp.filter_eq_sum

∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M),
  Finsupp.filter p f = ∑ i ∈ f.support with p i, fun₀ | i => f i

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidablePred