Commit 2025-03-27 12:28 da234f84

View on Github →

feat: other form of the LYM inequality (#22633) and use semantic names for the existing lemmas. Moves:

  • card_mul_le_card_shadow_mullocal_lubell_yamamoto_meshalkin_inequality_mul
  • card_div_choose_le_card_shadow_div_chooselocal_lubell_yamamoto_meshalkin_inequality_div
  • sum_card_slice_div_choose_le_onelubell_yamamoto_meshalkin_inequality_sum_card_div_choose From PlainCombi (LeanCamCombi)

Estimated changes