Theorems · Theorem · order theory

IncidenceAlgebra.eulerChar_prod

∀ (𝕜 : Type u_2) {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : PartialOrder β]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : LocallyFiniteOrder β] [inst_5 : DecidableEq α] [inst_6 : DecidableEq β]
  [inst_7 : DecidableLE α] [inst_8 : DecidableLE β] [inst_9 : BoundedOrder α] [inst_10 : BoundedOrder β],
  IncidenceAlgebra.eulerChar 𝕜 (α × β) = IncidenceAlgebra.eulerChar 𝕜 α * IncidenceAlgebra.eulerChar 𝕜 β

Defined in

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingPartialOrderPartialOrderLocallyFiniteOrderLocallyFiniteOrderDecidableEqDecidableEqDecidableLEDecidableLEBoundedOrderBoundedOrder