Theorem cauchy_davenport_mul_of_isTorsionFree

Modification history

2025-07-27 09:45

Mathlib/Combinatorics/Additive/CauchyDavenport.lean

chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (#24311) …

Deleted cauchy_davenport_mul_of_isTorsionFree View on Github →

2024-11-07 15:42

Mathlib/Combinatorics/Additive/CauchyDavenport.lean

chore(CauchyDavenport): use semantic lemma names (#17697) …

Added cauchy_davenport_mul_of_isTorsionFree View on Github →