chore: restore and deprecate Mathlib.Combinatorics.Enumerative.Partition (#31677)

wwylele · wwylele · commit 41c8cd5fe182 · 2025-11-16T13:56:21.000Z
This was previously moved in #30567
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3024,6 +3024,7 @@ import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Combinatorics.Enumerative.DyckWord
 import Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
 import Mathlib.Combinatorics.Enumerative.InclusionExclusion
+import Mathlib.Combinatorics.Enumerative.Partition
 import Mathlib.Combinatorics.Enumerative.Partition.Basic
 import Mathlib.Combinatorics.Enumerative.Partition.GenFun
 import Mathlib.Combinatorics.Enumerative.Stirling
diff --git a/Mathlib/Combinatorics/Enumerative/Partition.lean b/Mathlib/Combinatorics/Enumerative/Partition.lean
@@ -0,0 +1,3 @@
+import Mathlib.Combinatorics.Enumerative.Partition.Basic
+
+deprecated_module (since := "2025-11-15")

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+import Mathlib.Combinatorics.Enumerative.Partition.Basic`
	`2`	`+`
	`3`	`+deprecated_module (since := "2025-11-15")`