Commit 2025-01-21 15:48 ed194772

View on Github →

feat(IncidenceAlgebra): Euler characteristic of a partial order (#20299) From LeanCamCombi

Estimated changes

Modified Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

added def IncidenceAlgebra.eulerChar

added theorem IncidenceAlgebra.eulerChar_orderDual

added theorem IncidenceAlgebra.eulerChar_prod

Modified Mathlib/Order/BoundedOrder/Basic.lean

modified theorem Prod.fst_bot

modified theorem Prod.fst_top

modified theorem Prod.snd_bot

modified theorem Prod.snd_top