Theorems · Definition · order theory

IncidenceAlgebra.mu

(𝕜 : Type u_2) →
  {α : Type u_5} →
    [inst : AddCommGroup 𝕜] →
      [One 𝕜] → [inst_2 : Preorder α] → [LocallyFiniteOrder α] → [DecidableEq α] → IncidenceAlgebra 𝕜 α

The Möbius function which inverts zeta as an element of the incidence algebra.

Defined in

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Cited by

15 results in Mathlib

Foundations

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

Assumes

AddCommGroupOnePreorderLocallyFiniteOrderDecidableEq