cauchy_davenport_of_isMulTorsionFree

English

In a torsion-free group, the CD bound holds: for nonempty finite s,t, |s|+|t|−1 ≤ |s t|.

Русский

В торсионно-бесконечной группе теорема CD: для непустых конечных s,t выполняется |s|+|t|−1 ≤ |s t|.

LaTeX

$$$|s|+|t|-1 \\le |s t|.$$$

Lean4

/-- The **Cauchy-Davenport Theorem** for torsion-free groups. The size of `s * t` is lower-bounded
by `|s| + |t| - 1`. -/
@[to_additive /-- The **Cauchy-Davenport theorem** for torsion-free groups. The size of `s + t` is lower-bounded
    by `|s| + |t| - 1`. -/
    ]
theorem cauchy_davenport_of_isMulTorsionFree [DecidableEq G] [Group G] [IsMulTorsionFree G] {s t : Finset G}
    (hs : s.Nonempty) (ht : t.Nonempty) : #s + #t - 1 ≤ #(s * t) := by
  simpa only [Monoid.minOrder_eq_top, min_eq_right, le_top, Nat.cast_le] using cauchy_davenport_minOrder_mul hs ht

Похожие утверждения