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_mul
→local_lubell_yamamoto_meshalkin_inequality_mul
card_div_choose_le_card_shadow_div_choose
→local_lubell_yamamoto_meshalkin_inequality_div
sum_card_slice_div_choose_le_one
→lubell_yamamoto_meshalkin_inequality_sum_card_div_choose
From PlainCombi (LeanCamCombi)