Theorems · Definition · order theory

IncidenceAlgebra.eulerChar

(𝕜 : Type u_2) →
  (α : Type u_5) →
    [AddCommGroup 𝕜] → [One 𝕜] → [inst : Preorder α] → [LocallyFiniteOrder α] → [DecidableEq α] → [BoundedOrder α] → 𝕜

The Euler characteristic of a finite bounded order.

Defined in

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Cited by

2 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupOnePreorderLocallyFiniteOrderDecidableEqBoundedOrder