card_small_parts_eq_mod — Mathlib

English

The number of small parts equals |P.parts| - (|s| mod |P.parts|).

Русский

Число малых частей равно |P.parts| - (|s| мод |P.parts|).

LaTeX

$$#({p ∈ P.parts | #p = #s / #P.parts}) = #P.parts - #s % #P.parts$$

Lean4

/-- An equipartition of a finset with `n` elements into `k` parts has
`n - n % k` parts of size `n / k`. -/
theorem card_small_parts_eq_mod (hP : P.IsEquipartition) :
    #({p ∈ P.parts | #p = #s / #P.parts}) = #P.parts - #s % #P.parts :=
  by
  conv_rhs =>
    arg 1
    rw [← filter_card_add_filter_neg_card_eq_card (p := fun p ↦ #p = #s / #P.parts + 1)]
  rw [hP.card_large_parts_eq_mod, add_tsub_cancel_left, hP.filter_ne_average_add_one_eq_average]

Похожие утверждения