Theorems · Theorem · group theory

Finset.sum_apply_ite_of_false

∀ {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [inst : AddCommMonoid M] {p : ι → Prop}
  [inst_1 : DecidablePred p] (f g : ι → γ) (k : γ → M),
  (∀ x ∈ s, ¬p x) → ∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (g x)

Defined in: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Cited by: 0 results in Mathlib
Foundations: Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommMonoid DecidablePred

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Finsetstatement and proof · cited by 13,712
AddCommMonoidstatement and proof · cited by 12,281
Finset.sumstatement and proof · cited by 5,195
Finset.sum_congrproof · cited by 2,323
Finset.sum_ite_of_falseproof · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.