Theorem Monoid.IsTorsionFree.card_add_card_sub_one_le_card_mul

Modification history

2024-11-07 15:42
Mathlib/Combinatorics/Additive/CauchyDavenport.lean
chore(CauchyDavenport): use semantic lemma names (#17697) …
Deleted Monoid.IsTorsionFree.card_add_card_sub_one_le_card_mulView on Github →
2023-12-08 15:24
Mathlib/Combinatorics/SetFamily/CauchyDavenport.lean
feat: The Cauchy-Davenport theorem (#8429) …
Added Monoid.IsTorsionFree.card_add_card_sub_one_le_card_mulView on Github →