Theorems · Theorem · combinatorics

Finpartition.IsEquipartition.card_large_parts_eq_mod

∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {P : Finpartition s},
  P.IsEquipartition → {p ∈ P.parts | p.card = s.card / P.parts.card + 1}.card = s.card % P.parts.card

An equipartition of a finset with n elements into k parts has n % k parts of size n / k + 1.

Defined in

Mathlib.Order.Partition.Equipartition

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEq