prod_one

Mathlib.Data.DFinsupp.BigOperators

URI: https://scilib.ai/kg/mathlib#DFinsupp.prod_one

← MathLib Explorer

English

The product of 1 across all coordinates equals 1.

Русский

Произведение единиц по всем координатам равно единице.

LaTeX

$$$\\left( f.prod (\\\\lambda i _ . 1) \\\\right) = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_one [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ i, β i} :
    (f.prod fun _ _ => (1 : γ)) = 1 :=
  Finset.prod_const_one

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

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

Разделы

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

Аффилиация

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