finprod_mem_of_eqOn_one — Mathlib

English

If f equals 1 on s, then the finprod over s of f is 1.

Русский

Если f(x)=1 на s, то ∏ᶠ i∈s f(i)=1.

LaTeX

$$$\\displaystyle s.EqOn\\ f\\ 1 \\Rightarrow \\prod\\ᶠ i \\in s, f(i) = 1$$$

Lean4

/-- If a function `f` equals `1` on a set `s`, then the product of `f i` over `i ∈ s` equals `1`. -/
@[to_additive /-- If a function `f` equals `0` on a set `s`, then the sum of `f i` over `i ∈ s`
          equals `0`. -/
    ]
theorem finprod_mem_of_eqOn_one (hf : s.EqOn f 1) : ∏ᶠ i ∈ s, f i = 1 :=
  by
  rw [← finprod_mem_one s]
  exact finprod_mem_congr rfl hf

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