Commit 2024-11-07 15:42 de9244e9

View on Github →

chore(CauchyDavenport): use semantic lemma names (#17697) The symbol-reading names were super long and mis-additivised. Also move the file to Combinatorics.Additive. It has nothing to do in Combinatorics.SetFamily

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Combinatorics/SetFamily/CauchyDavenport.lean to Mathlib/Combinatorics/Additive/CauchyDavenport.lean

deleted theorem Finset.card_add_card_sub_one_le_card_mul

deleted theorem Finset.min_le_card_mul

deleted theorem Monoid.IsTorsionFree.card_add_card_sub_one_le_card_mul

added theorem ZMod.cauchy_davenport

deleted theorem ZMod.min_le_card_add

added theorem cauchy_davenport_minOrder_mul

added theorem cauchy_davenport_mul_of_isTorsionFree

added theorem cauchy_davenport_mul_of_linearOrder_isCancelMul