card_mod_card_parts_le — Mathlib

English

For the same setup, |s| mod |P.parts| ≤ |P.parts| holds as a general bound, with the special case handling when the number of parts is zero.

Русский

LaTeX

$$$|s| \\% |P.parts| \\le |P.parts|$$

Lean4

theorem card_mod_card_parts_le : #s % #P.parts ≤ #P.parts :=
  by
  obtain h | h := (#P.parts).eq_zero_or_pos
  · rw [h]
    rw [Finset.card_eq_zero, parts_eq_empty_iff, bot_eq_empty, ← Finset.card_eq_zero] at h
    rw [h]
  · exact (Nat.mod_lt _ h).le

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