prod_filter_ne_one — Mathlib

English

A specialization of the filter lemma when we filter by predicate p and require f(x) ≠ 1 for attention; the equality with the full product holds.

Русский

Специализация леммы о фильтре при предикате p и условии f(x) ≠ 1 сохраняет равенство с полным произведением.

LaTeX

$$$\prod_{x\in s with p x} f x = \prod_{x\in s} f x$$$

Lean4

@[to_additive]
theorem prod_filter_ne_one (s : Finset ι) [∀ x, Decidable (f x ≠ 1)] : ∏ x ∈ s with f x ≠ 1, f x = ∏ x ∈ s, f x :=
  prod_filter_of_ne fun _ _ => id

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