tprod_eq_one_iff — Mathlib

English

If the infinite product ∏' i, f(i) equals 1, then every term f(i) equals 1; conversely, if every f(i) equals 1, the product equals 1.

Русский

Если бесконечное произведение ∏' i, f(i) равно 1, то каждый член f(i) равен 1; наоборот, если все f(i) равны 1, то произведение равно 1.

LaTeX

$$$\\\\prod' i \\, f(i) = 1 \\\\iff \\\\forall i \\, f(i) = 1$$$

Lean4

@[to_additive]
protected theorem tprod_eq_one_iff (hf : Multipliable f) : ∏' i, f i = 1 ↔ ∀ x, f x = 1 := by
  rw [← hasProd_one_iff, hf.hasProd_iff]

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