Theorems · Definition · order theory

IncidenceAlgebra.toFun

{𝕜 : Type u_7} → {α : Type u_8} → [inst : Zero 𝕜] → [inst_1 : LE α] → IncidenceAlgebra 𝕜 α → α → α → 𝕜

The underlying function of an element of the incidence algebra. Do not use this function directly. Instead use the coercion coming from the FunLike instance.

Defined in: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
Cited by: 2 results in Mathlib
Foundations: Depth 2 from the axioms · uses no axioms
Assumes: Zero LE

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

IncidenceAlgebrastatement and proof · cited by 51

Cited by2

Results whose statement or proof uses this declaration.

IncidenceAlgebra.eq_zero_of_not_le'statement · cited by 1
IncidenceAlgebra.toFun_eq_coestatement · cited by 0