feat: Port Combinatorics.Pigeonhole (#1758)

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
leanprover-community · Jan 23, 2023 · 5742ec1 · 5742ec1
1 parent c40a401
commit 5742ec1
Show file tree

Hide file tree

Showing 2 changed files with 482 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -207,6 +207,7 @@ import Mathlib.CategoryTheory.Whiskering
 import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Combinatorics.DoubleCounting
 import Mathlib.Combinatorics.Hall.Finite
+import Mathlib.Combinatorics.Pigeonhole
 import Mathlib.Combinatorics.Quiver.Arborescence
 import Mathlib.Combinatorics.Quiver.Basic
 import Mathlib.Combinatorics.Quiver.Cast