Theorem cauchy_davenport_mul_of_linearOrder_isCancelMul

Modification history

2025-03-23 20:22
Mathlib/Combinatorics/Additive/CauchyDavenport.lean
feat: generalize Mathlib.Combinatorics (#23185) …
Modified cauchy_davenport_mul_of_linearOrder_isCancelMulView on Github →
2024-11-07 15:42
Mathlib/Combinatorics/Additive/CauchyDavenport.lean
chore(CauchyDavenport): use semantic lemma names (#17697) …
Added cauchy_davenport_mul_of_linearOrder_isCancelMulView on Github →