tprod_eq_zero_mul — Mathlib

English

For a topological monoid G with T2 separation and f: ℕ → G multipliable, the full product equals f(0) times the tail product: ∏' i, f i = f(0) · ∏' i, f(i+1).

Русский

Пусть G — топологический моноид с диагональной сходимостью; если f: ℕ → G мультиплируемо, то полное произведение равно f(0) умножить на хвостовое произведение: ∏' i, f i = f(0) · ∏' i, f(i+1).

LaTeX

$$$\prod' b, f b = f 0 \cdot \prod' b, f (b+1)$$$

Lean4

@[to_additive]
protected theorem tprod_eq_zero_mul [T2Space G] {f : ℕ → G} (hf : Multipliable f) : ∏' b, f b = f 0 * ∏' b, f (b + 1) :=
  tprod_eq_zero_mul' <| (multipliable_nat_add_iff 1).2 hf

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