prod_toFinset_eq_subtype — Mathlib

English

Let M be a commutative monoid, α finite, p a predicate on α, f: α → M. Then the product over a ∈ {x | p x}.toFinset of f a equals the product over a : Subtype p of f a.

Русский

Пусть M — коммутативный моноид, α конечен, p — предикат на α, f: α → M. Тогда произведение по a ∈ {x | p x}.toFinset от f a равно произведению по a : Subtype p от f a.

LaTeX

$$$ \\displaystyle \\prod a \\in \\{x \\mid p x\\}.toFinset, f a = \\prod a : \\{ x \\mid p x \\}, f a.$$$

Lean4

@[to_additive]
theorem prod_toFinset_eq_subtype {M : Type*} [CommMonoid M] [Fintype α] (p : α → Prop) [DecidablePred p] (f : α → M) :
    ∏ a ∈ {x | p x}.toFinset, f a = ∏ a : Subtype p, f a :=
  by
  rw [← Finset.prod_subtype]
  simp_rw [Set.mem_toFinset]; intro; rfl

Похожие утверждения