Theorems · Theorem · combinatorics

Finset.prod_powerset_insert

∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} [inst : CommMonoid β] [inst_1 : DecidableEq α],
  a ∉ s →
    ∀ (f : Finset α → β), ∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

A product over all subsets of s ∪ {x} is obtained by multiplying the product over all subsets of s, and over all subsets of s to which one adds x.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidDecidableEq