Theorems · Theorem · group theory

Finset.sum_congr_of_eq_on_inter

∀ {ι : Type u_5} {M : Type u_6} {s₁ s₂ : Finset ι} {f g : ι → M} [inst : AddCommMonoid M],
  (∀ a ∈ s₁, a ∉ s₂ → f a = 0) →
    (∀ a ∈ s₂, a ∉ s₁ → g a = 0) → (∀ a ∈ s₁, a ∈ s₂ → f a = g a) → ∑ a ∈ s₁, f a = ∑ a ∈ s₂, g a

The sum of two functions f g : ι → M over finite sets s₁ s₂ : Finset ι are equal if the functions agree on s₁ ∩ s₂, f = 0 and g = 0 on the respective set differences.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddCommMonoid