Theorems · Theorem · order theory

Prod.card_box_succ

∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : Ring β]
  [inst_4 : PartialOrder β] [IsOrderedRing β] [inst_6 : LocallyFiniteOrder α] [inst_7 : LocallyFiniteOrder β]
  [inst_8 : DecidableEq α] [inst_9 : DecidableEq β] [inst_10 : DecidableLE (α × β)] (n : ℕ),
  (Finset.box (n + 1)).card =
    (Finset.Icc (-↑n.succ) ↑n.succ).card * (Finset.Icc (-↑n.succ) ↑n.succ).card -
      (Finset.Icc (-↑n) ↑n).card * (Finset.Icc (-↑n) ↑n).card

Defined in

Mathlib.Order.Interval.Finset.Box

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingPartialOrderIsOrderedRingRingPartialOrderIsOrderedRingLocallyFiniteOrderLocallyFiniteOrderDecidableEqDecidableEqDecidableLE