English
Let s be a finite set and f: ι → M a function into a monoid M. For a predicate p: ι → Prop and a decidable predicate, if for all x ∈ s, f(x) ≠ 1 implies p(x), then filtering s by p does not change the product: ∏ x∈s with p x, f x = ∏ x∈s, f x.
Русский
Пусть s—конечное множество, f: ι → M — функция в моноид M. Пусть p: ι → Prop. Если для любого x ∈ s верно: f(x) ≠ 1 → p(x), тогда произведение над s с фильтром p равно произведению по всем x∈s: ∏ x∈s with p x, f x = ∏ x∈s, f x.
LaTeX
$$$\prod_{x \in s \text{ with } p x} f(x) = \prod_{x \in s} f(x)$$$
Lean4
@[to_additive]
theorem prod_filter_of_ne {p : ι → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 1 → p x) :
∏ x ∈ s with p x, f x = ∏ x ∈ s, f x :=
(prod_subset (filter_subset _ _)) fun x => by
classical
rw [not_imp_comm, mem_filter]
exact fun h₁ h₂ =>
⟨h₁, by simpa using hp _ h₁ h₂⟩
-- If we use `[DecidableEq M]` here, some rewrites fail because they find a wrong `Decidable`
-- instance first; `{∀ x, Decidable (f x ≠ 1)}` doesn't work with `rw ← prod_filter_ne_one`
