Theorems · Theorem · group theory

finprod_mem_powerset_diff_elem

Deprecated since 2026-06-03Use finprod_mem_powerset_sdiff_elem instead.

∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : Set α → M} {s : Set α} {a : α},
  s.Finite →
    a ∈ s →
      ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t =
        (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t)

Alias of finprod_mem_powerset_sdiff_elem.

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoid