tsum_congr_cofinite₀ — Mathlib

English

If f is Multipliable and agrees with g outside a finite set s, then the sum over g equals the product over f times the finite-ratio factor:

Русский

Если f можно умножать в совокупности и функцией g совпадает с f вне конечного множества s, тогда сумма по g равна сумме по f, умноженной на конечный коэффициент отношения.

LaTeX

$$$$ \prod' i, g i = \Big(\prod' i, f i\Big) \cdot\frac{\prod_{i \in s} g i}{\prod_{i \in s} f i}.$$$$

Lean4

protected theorem tsum_congr_cofinite₀ [T2Space K] (hc : Multipliable f) {s : Finset α} (hs : ∀ a ∈ s, f a ≠ 0)
    (hs' : ∀ a ∉ s, f a = g a) : ∏' i, g i = ((∏' i, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)) :=
  (hc.hasProd.congr_cofinite₀ hs hs').tprod_eq

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