Commit 2024-07-15 06:14 ce90d358
View on Github →chore(Combinatorics/Additive/PluenneckeRuzsa): Use semantic lemma names (#13329) I, as the main author of those theorems, can never remember their names. Symbol-reading as a naming convention fails here because there are too many symbols to mention to
- distinguish the series of results from other results in Mathlib
- distinguish the different results within that series Using semantic names solves both issues quite nicely.