Commit 2025-07-03 04:49 fd24e4a3
View on Github →feat(Combinatorics/Additive): trivial bounds on doubling constant (#26636) Add trivial upper and lower bounds on the doubling and difference constants. Renames:
div_card_le
->card_div_le
feat(Combinatorics/Additive): trivial bounds on doubling constant (#26636) Add trivial upper and lower bounds on the doubling and difference constants. Renames:
div_card_le
-> card_div_le