Commit 2024-03-29 15:34 056bc615
View on Github →chore(Combinatorics/Additive/PluenneckeRuzsa): add @to_additive to various formulations of Ruzsa's triangle inequality (#11766)
Add @to_additive to card_mul_mul_le_card_div_mul_card_div, card_div_mul_le_card_mul_mul_card_div and card_sub_mul_card_le_card_sub_mul_card_add and correct their documentation.