hasProd_ite_div_hasProd — Mathlib

English

If the infinite product ∏' f(b) over β converges to a, then replacing the b-th factor by 1 yields a product converging to a / f(b).

Русский

Если бесконечное произведение по β сходится к a, то замена фактора в позиции b на 1 приводит к произведению, сходящемуся к a / f(b).

LaTeX

$$$\\text{HasProd}\\bigl(\\lambda n.\\, \\operatorname{ite}(n=b)\,1\\, (f(n))\\bigr)\\;=\\; a/f(b).$$$

Lean4

@[to_additive]
theorem hasProd_ite_div_hasProd [L.LeAtTop] [DecidableEq β] (hf : HasProd f a L) (b : β) :
    HasProd (fun n ↦ ite (n = b) 1 (f n)) (a / f b) L :=
  by
  convert hf.update b 1 using 1
  · ext n
    rw [Function.update_apply]
  · rw [div_mul_eq_mul_div, one_mul]

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