davenport_constant_groups
Provedalgebracombinatoricscomputational-complexity
Davenport constant: For cyclic groups ℤₙ, the Davenport constant D(ℤₙ) = 2n-1 (every sequence of 2n-1 elements has a nonempty zero-sum subsequence). For general finite groups, D(G) is determined by the structure of G. Open for some group families.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem davenport_constant_groups (n : ℕ) (hn : 1 ≤ n) :
∃ (D : ℕ), D = 2 * n - 1 ∧
∀ (seq : Fin D → ZMod n),
∃ (I : Finset (Fin D)) (_ : I.Nonempty),
(I.sum seq) = 0 := by
sorrySource