tprod_div — Mathlib

English

If f and g are multipliable, then the tprod of f(b)/g(b) equals the quotient of the tprod of f by the tprod of g.

Русский

Если обе функции умножаемы, то бесконечное произведение отношения является отношением бесконечных произведений: ∏ (f/g) = (∏ f)/(∏ g).

LaTeX

$$$\prod'_{L} b, \frac{f(b)}{g(b)} = \frac{\prod'_{L} b, f(b)}{\prod'_{L} b, g(b)}.$$$

Lean4

@[to_additive]
protected theorem tprod_div [L.NeBot] (hf : Multipliable f L) (hg : Multipliable g L) :
    ∏'[L] b, (f b / g b) = (∏'[L] b, f b) / ∏'[L] b, g b :=
  (hf.hasProd.div hg.hasProd).tprod_eq

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