module docs

src/combinatorics/additive/cauchy_davenport.lean

@@ -10,7 +10,23 @@ import set_theory.cardinal.finite
 /-!
 # The Cauchy-Davenport theorem
 
+This file proves the Cauchy-Davenport theorem as a corollary to a more general result.
 
+## Main declarations
+
+* `subgroup.nontrivial_size`: The minimum size of a finite nontrivial subgroup of a given group. If
+  the group is trivial, it is `1` by convention.
+* `finset.card_add_card_sub_one_le_min_nontrivial_size_card_mul`: A generalisation of Károlyi's
+  theorem.
+* `zmod.card_add_card_sub_one_le_min_card_add_zmod`: The Cauchy-Davenport theorem.
+
+## References
+
+* Matt DeVos, *On a generalization of the Cauchy-Davenport theorem*
+
+## Tags
+
+additive combinatorics, sumset, karolyi, cauchy-davenport, number theory
 -/
 
 namespace subgroup
@@ -79,9 +95,9 @@ begin
   { refine ⟨b⁻¹ * a, _, mem_inter.2 ⟨mem_smul_finset.2 ⟨_, hb, _⟩, ha⟩⟩,
     simp },
   obtain hgs | hgs := eq_or_ne (g • s) s,
-  { refine min_le_of_left_le (le_trans _ $ card_le_card_mul_right _ ht),
     obtain ⟨S, hS⟩ : ∃ S : subgroup α, (S : set α) ⊆ s := sorry,
-    refine (nontrivial_size_le_nat_card $ s.finite_to_set.subset hS).trans _,
+  { refine min_le_of_left_le ((nontrivial_size_le_nat_card $ s.finite_to_set.subset hS).trans $
+      le_trans _ $ card_le_card_mul_right _ ht),
     sorry },
   sorry,
 end

src/combinatorics/additive/kneser.lean

@@ -14,12 +14,12 @@ This file proves Kneser's theorem. This states that `|s + H| + |t + H| - |H| ≤
 
 ## Main declarations
 
-* `finset.mul_stab`: The stabilizer of a **nonempty** finset as a finset.
 * `finset.mul_kneser`: Kneser's theorem.
 
 ## References
 
 * [Imre Ruzsa, *Sumsets and structure*][ruzsa2009]
+* Matt DeVos, *A short proof of Kneser's addition theorem*
 -/
 
 open function mul_action

src/combinatorics/additive/mathlib.lean

@@ -7,6 +7,12 @@ import data.finset.pointwise
 import data.set.pointwise.finite
 import group_theory.quotient_group
 
+/-!
+# For mathlib
+
+A lot of stuff to move
+-/
+
 namespace function
 variables {α β γ : Type*}