Theory Cauchy_Davenport_Entry

theory Cauchy_Davenport_Entry
  imports
    Modular_Sumsets
    Cauchy_Davenport_Prime_Field
    Vosper_Prime_Field
begin

section ‹Overview›

text ‹
  This section records the scope of the combined Cauchy-Davenport and Vosper
  development. The session combines abstract prime-field sumset theorems with
  concrete representative lemmas for modular sumsets. The resulting theory stack
  connects generic finite-sumset infrastructure, the polynomial-method
  Cauchy-Davenport bound, and the final Vosper classification theorem.
›

end