feat: port Combinatorics.Additive.Behrend (#4730)

leanprover-community · Jun 6, 2023 · 6dea3c8 · 6dea3c8
1 parent 9f0fbd0
commit 6dea3c8
Show file tree

Hide file tree

Showing 2 changed files with 562 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -980,6 +980,7 @@ import Mathlib.CategoryTheory.Types
 import Mathlib.CategoryTheory.Whiskering
 import Mathlib.CategoryTheory.WithTerminal
 import Mathlib.CategoryTheory.Yoneda
+import Mathlib.Combinatorics.Additive.Behrend
 import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Combinatorics.Additive.Etransform
 import Mathlib.Combinatorics.Additive.PluenneckeRuzsa