one_prod_one

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

URI: https://scilib.ai/kg/mathlib#IncidenceAlgebra.one_prod_one

← MathLib Explorer

English

The product of unit elements in the two-incidence-algebra product is the unit: (prod 1 1) = 1.

Русский

Произведение единиц в двухинцидентной алгебре равно единице: (prod 1 1) = 1.

LaTeX

$$$ (\mathrm{prod}\ 1\ 1) = 1 $$$

Lean4

@[simp]
theorem one_prod_one [DecidableEq α] [DecidableEq β] : (.prod 1 1 : IncidenceAlgebra 𝕜 (α × β)) = 1 := by ext x y;
  simp [Prod.ext_iff, ← ite_and, and_comm]

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

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

Разделы

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

Аффилиация

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