hasProd_iff — Mathlib

English

Suppose f is Multipliable along L. Then HasProd f a L holds if and only if the infinite product ∏'[L] b, f b equals a.

Русский

Пусть f является Multipliable вдоль L. Тогда HasProd f a L выполняется тогда, когда бесконечное произведение ∏'[L] b, f(b) равно a.

LaTeX

$$(h : Multipliable f L) ⟂ HasProd f a L ↔ ∏'[L] b, f b = a$$

Lean4

@[to_additive]
theorem hasProd_iff (h : Multipliable f L) : HasProd f a L ↔ ∏'[L] b, f b = a :=
  Iff.intro HasProd.tprod_eq fun eq ↦ eq ▸ h.hasProd

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