Theorems · Theorem · group theory

Finset.prod_congr_set

∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Fintype ι] (s : Set ι)
  [inst_2 : DecidablePred fun x => x ∈ s] (f : ι → M) (g : ↑s → M),
  (∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩) → (∀ x ∉ s, f x = 1) → ∏ i, f i = ∏ i, g i

The product of a function g defined only on a set s is equal to the product of a function f defined everywhere, as long as f and g agree on s, and f = 1 off s.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidFintypeDecidablePred