move(Combinatorics/Enumerative): Create folder (#11666)

Move `Catalan`, `Composition`, `DoubleCounting`, `Partition` to a new folder `Combinatorics.Enumerative`.
leanprover-community · Mar 26, 2024 · eec91f3 · eec91f3
1 parent dda2b3f
commit eec91f3
Show file tree

Hide file tree

Showing 11 changed files with 11 additions and 11 deletions.
diff --git a/Archive/Wiedijk100Theorems/Partition.lean b/Archive/Wiedijk100Theorems/Partition.lean
@@ -5,7 +5,7 @@ Authors: Bhavik Mehta, Aaron Anderson
 -/
 import Mathlib.RingTheory.PowerSeries.Inverse
 import Mathlib.RingTheory.PowerSeries.Order
-import Mathlib.Combinatorics.Partition
+import Mathlib.Combinatorics.Enumerative.Partition
 import Mathlib.Data.Nat.Parity
 import Mathlib.Data.Finset.NatAntidiagonal
 import Mathlib.Data.Fin.Tuple.NatAntidiagonal

diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1447,20 +1447,20 @@ import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Combinatorics.Additive.PluenneckeRuzsa
 import Mathlib.Combinatorics.Additive.RuzsaCovering
 import Mathlib.Combinatorics.Additive.SalemSpencer
-import Mathlib.Combinatorics.Catalan
 import Mathlib.Combinatorics.Colex
-import Mathlib.Combinatorics.Composition
 import Mathlib.Combinatorics.Configuration
 import Mathlib.Combinatorics.Derangements.Basic
 import Mathlib.Combinatorics.Derangements.Exponential
 import Mathlib.Combinatorics.Derangements.Finite
-import Mathlib.Combinatorics.DoubleCounting
+import Mathlib.Combinatorics.Enumerative.Catalan
+import Mathlib.Combinatorics.Enumerative.Composition
+import Mathlib.Combinatorics.Enumerative.DoubleCounting
+import Mathlib.Combinatorics.Enumerative.Partition
 import Mathlib.Combinatorics.HalesJewett
 import Mathlib.Combinatorics.Hall.Basic
 import Mathlib.Combinatorics.Hall.Finite
 import Mathlib.Combinatorics.Hindman
 import Mathlib.Combinatorics.Optimization.ValuedCSP
-import Mathlib.Combinatorics.Partition
 import Mathlib.Combinatorics.Pigeonhole
 import Mathlib.Combinatorics.Quiver.Arborescence
 import Mathlib.Combinatorics.Quiver.Basic

diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Johan Commelin
 -/
 import Mathlib.Analysis.Analytic.Basic
-import Mathlib.Combinatorics.Composition
+import Mathlib.Combinatorics.Enumerative.Composition
 
 #align_import analysis.analytic.composition from "leanprover-community/mathlib"@"ce11c3c2a285bbe6937e26d9792fda4e51f3fe1a"
 

diff --git a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies, George Shakan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, George Shakan
 -/
-import Mathlib.Combinatorics.DoubleCounting
+import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Data.Finset.Pointwise
 import Mathlib.Data.NNRat.Lemmas
 import Mathlib.Tactic.GCongr

diff --git a/Mathlib/Combinatorics/Catalan.lean → ...ib/Combinatorics/Enumerative/Catalan.lean b/Mathlib/Combinatorics/Catalan.lean → ...ib/Combinatorics/Enumerative/Catalan.lean
diff --git a/Mathlib/Combinatorics/Composition.lean → ...ombinatorics/Enumerative/Composition.lean b/Mathlib/Combinatorics/Composition.lean → ...ombinatorics/Enumerative/Composition.lean
diff --git a/Mathlib/Combinatorics/DoubleCounting.lean → ...inatorics/Enumerative/DoubleCounting.lean b/Mathlib/Combinatorics/DoubleCounting.lean → ...inatorics/Enumerative/DoubleCounting.lean
diff --git a/Mathlib/Combinatorics/Partition.lean → .../Combinatorics/Enumerative/Partition.lean b/Mathlib/Combinatorics/Partition.lean → .../Combinatorics/Enumerative/Partition.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
-import Mathlib.Combinatorics.Composition
+import Mathlib.Combinatorics.Enumerative.Composition
 import Mathlib.Data.Nat.Parity
 import Mathlib.Tactic.ApplyFun
 

diff --git a/Mathlib/Combinatorics/SetFamily/LYM.lean b/Mathlib/Combinatorics/SetFamily/LYM.lean
@@ -5,7 +5,7 @@ Authors: Bhavik Mehta, Alena Gusakov, Yaël Dillies
 -/
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.Order.Field.Basic
-import Mathlib.Combinatorics.DoubleCounting
+import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Combinatorics.SetFamily.Shadow
 import Mathlib.Data.Rat.Order
 

diff --git a/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean b/Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Alena Gusakov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alena Gusakov, Jeremy Tan
 -/
-import Mathlib.Combinatorics.DoubleCounting
+import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
 import Mathlib.Combinatorics.SimpleGraph.Basic
 import Mathlib.Data.Set.Finite

diff --git a/Mathlib/GroupTheory/Perm/Cycle/Type.lean b/Mathlib/GroupTheory/Perm/Cycle/Type.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 import Mathlib.Algebra.GCDMonoid.Multiset
-import Mathlib.Combinatorics.Partition
+import Mathlib.Combinatorics.Enumerative.Partition
 import Mathlib.Data.List.Rotate
 import Mathlib.GroupTheory.Perm.Cycle.Factors
 import Mathlib.GroupTheory.Perm.Closure