eulerChar

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

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

English

For any a, μ(a,a) = 1.

Русский

Для любого a: μ(a,a) = 1.

LaTeX

$$$ μ 𝕜 a a = 1 $$$

Lean4

/-- The Euler characteristic of a finite bounded order. -/
def eulerChar [BoundedOrder α] : 𝕜 :=
  mu 𝕜 (⊥ : α) ⊤

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

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

Разделы

Аффилиация

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