Theorems · Theorem · group theory

finprod_mem_powerset_sdiff_elem

∀ {α : 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)

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoid