tprod_eq

Mathlib.Topology.Algebra.InfiniteSum.Defs

URI: https://scilib.ai/kg/mathlib#HasProd.tprod_eq

English

If ha is a HasProd for f with value a in L, then the infinite product ∏'[L] b, f b equals a.

Русский

Если ha — HasProd f a L, то бесконечное произведение ∏'[L] b, f(b) равно a.

LaTeX

$$ha : HasProd f a L ⟶ ∏'[L] b, f b = a$$

Lean4

@[to_additive]
theorem tprod_eq (ha : HasProd f a L) : ∏'[L] b, f b = a :=
  (Multipliable.hasProd ⟨a, ha⟩).unique ha

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru