Theorems · Theorem · group theory

Finset.prod_congr_of_eq_on_inter

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

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

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommMonoid