finprod_unique

Mathlib.Algebra.BigOperators.Finprod

URI: https://scilib.ai/kg/mathlib#finprod_unique

← MathLib Explorer

English

If the type α is unique, then finprod f equals f default.

Русский

Если тип α единичен, то финпроизводство равно f по умолчанию.

LaTeX

$$$\\text{finprod}(f) = f(\\text{default})$ when $Unique\\, α$$$

Lean4

@[to_additive]
theorem finprod_unique [Unique α] (f : α → M) : ∏ᶠ i, f i = f default :=
  finprod_eq_single f default fun _x hx => (hx <| Unique.eq_default _).elim

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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