finprod_mem_one

Mathlib.Algebra.BigOperators.Finprod

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

← MathLib Explorer

English

The product of the constant 1 over any set equals 1.

Русский

Произведение по любому множеству константы 1 равно 1.

LaTeX

$$$\\displaystyle \\prod\\ᶠ i ∈ s, 1 = 1$$$

Lean4

/-- The product of the constant function `1` over any set equals `1`. -/
@[to_additive /-- The sum of the constant function `0` over any set equals `0`. -/
    ]
theorem finprod_mem_one (s : Set α) : (∏ᶠ i ∈ s, (1 : M)) = 1 := by simp

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

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

Разделы

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

Аффилиация

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