chore(Combinatorics): restore deprecated pentagonal.lean module

[wwylele]

---

• depends on: feat(PowerSeries): pentagonal number theorem #33143

[github-actions]

PR summary 03cb06d00e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.Enumerative.Pentagonal	1
Mathlib.Combinatorics.Enumerative.Pentagonal.Basic (new file)	513
Mathlib.Combinatorics.Enumerative.Pentagonal.Ring (new file)	1293
Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries (new file)	1463

---

Declarations diff (regex)

+ aux
+ aux_sub_aux
+ coeff_pentagonalSeries_eq_zero
+ coeff_pentagonalSeries_eq_zero_iff
+ coeff_pentagonalSeries_pentagonal
+ coeff_prod_one_sub_X_pow_eventually_eq
+ hasProd_one_sub_X_pow
+ hasSum_pentagonalSeries
+ hasSum_pow_pentagonal_sub_pentagonalSeries
+ multipliable_one_sub_X_pow
+ neg_one_pow_ne_zero
+ not_isNilpotent_neg_one
+ pentagonalSeries
+ pentagonalSeries_eq_tsum
+ pentagonalSeries_eq_tsum_pow_pentagonal_sub
+ powMulProdOneSubPow
+ summable_pow_mul_prod_one_sub_pow
+ tendsto_order_neg_X_pow
+ tendsto_order_pow_mul_prod_one_sub_pow
+ tprod_one_sub_X_pow
+ tprod_one_sub_X_pow'
+ tprod_one_sub_pow
+ tprod_one_sub_pow_eq_powMulProdOneSubPow
+ tprod_one_sub_pow_eq_powMulProdOneSubPow_zero
+ tsum_powMulProdOneSubPow

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 03cb06d00e
Reference commit 555b02bc95

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(PowerSeries): pentagonal number theorem #33143
  By Dependent Issues (🤖). Happy coding!