feat(MvPowerSeries/pderiv): add pderiv_map and pderiv_rename

[WenrongZou]

In this PR, we prove MvPowerSeries.map and MvPowerSeries.rename commute with taking derivative.

---

[github-actions]

PR summary c18d9ca93d

Import changes exceeding 2%

%	File
+45.40%	Mathlib.RingTheory.MvPowerSeries.Derivative

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.MvPowerSeries.Derivative	1381	2008	+627 (+45.40%)

Import changes for all files

Files	Import difference
12 files Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing Mathlib.NumberTheory.ModularForms.RamanujanFormula	27
Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.ZetaValues	33
Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli	34
Mathlib.RingTheory.PowerSeries.Exp Mathlib.RingTheory.PowerSeries.Log	99
Mathlib.RingTheory.PowerSeries.Derivative	341
Mathlib.RingTheory.MvPowerSeries.Derivative	627

---

Declarations diff (regex)

+ pderiv_map
+ pderiv_rename

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)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit c18d9ca).

• +2 new declarations
• −0 removed declarations

+MvPowerSeries.pderiv_map
+MvPowerSeries.pderiv_rename

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit c18d9ca93d
Reference commit 572e4d091b

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.py 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).