cauchy_davenport — Mathlib

English

IsApproximateSubgroup 1 A is equivalent to existence of a subgroup H with H = A (simplicity variant).

Русский

IsApproximateSubgroup 1 A эквивалентно существованию подпгруппы H, такой что H = A (упрощённая форма).

LaTeX

$$$\\IsApproximateSubgroup 1 A \\iff \\exists H: Subgroup G, H = A$$$

Lean4

/-- The **Cauchy-Davenport Theorem**. If `s`, `t` are nonempty sets in $$ℤ/pℤ$$, then the size of
`s + t` is lower-bounded by `|s| + |t| - 1`, unless this quantity is greater than `p`. -/
theorem cauchy_davenport {p : ℕ} (hp : p.Prime) {s t : Finset (ZMod p)} (hs : s.Nonempty) (ht : t.Nonempty) :
    min p (#s + #t - 1) ≤ #(s + t) := by
  simpa only [ZMod.minOrder_of_prime hp, min_le_iff, Nat.cast_le] using cauchy_davenport_minOrder_add hs ht

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