feat(RingTheory/MvPowerSeries): introduces various equivalences for MvPowerSeries

[BryceT233]

This PR introduces a number of equivalences related to power series rings and is patterned after Mathlib/Algebra/MvPolynomial/Equiv.lean.

To be specific, it adds:

• MvPowerSeries.isEmptyEquiv : The isomorphism between multivariable power series
  in no variables and the ground ring.

• MvPowerSeries.uniqueEquiv : The isomorphism between multivariable power series
  in a single variable and power series over the ground ring.

• MvPowerSeries.mapEquiv, MvPowerSeries.mapAlgEquiv : The isomorhism between
  multivariable power series induced by an isomorphism between the coefficient rings.

• MvPowerSeries.sumAlgEquiv : The isomorphism between multivariable power series
  in a sum of two types, and multivariable power series in one of the types,
  with coefficients in multivariable power series in the other type.

• MvPowerSeries.commAlgEquiv : The isomorphism between multivariable power series
  in variables σ of multivariable power series in variables τ and multivariable power series
  in variables τ of multivariable power series in variables σ.

• MvPowerSeries.optionEquivLeft : The isomorphism between multivariable power series
  in Option σ and power series with coefficients in MvPowerSeries σ R.

• MvPowerSeries.optionEquivRight : The isomorphism between multivariable power series
  in Option σ and multivariable power series in σ with coefficients in PowerSeries R

• MvPowerSeries.finSuccEquiv : The isomorphism between multivariable power series
  in Fin (n + 1) and power series over multivariable power series in Fin n.

---

• depends on: feat(Data/Finsupp): add computational lemmas for cons and single #35329
• depends on: [Merged by Bors] - feat(Data/Finsupp): add lemmas for Finsupp and Sum #36506

[github-actions]

PR summary b301d257a1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.MvPowerSeries.Equiv (new file)	1212

---

Declarations diff

+ coeff_coeff_finSuccEquiv
+ coeff_coeff_optionEquivLeft
+ coeff_coeff_optionEquivRight
+ coeff_coeff_optionFunLeft
+ coeff_coeff_optionFunRight
+ coeff_iterToSum
+ coeff_iterToSumFun
+ coeff_optionInvFunLeft
+ coeff_optionInvFunRight
+ coeff_sumToIter
+ coeff_sumToIterFun
+ coeff_uniqueEquiv
+ commAlgEquiv
+ commAlgEquiv_C
+ commAlgEquiv_C_X
+ commAlgEquiv_X
+ embDomain_finSuccEquiv_cons_eq_optionElim
+ finSuccEquiv
+ finSuccEquiv_X_succ
+ finSuccEquiv_X_zero
+ finSuccEquiv_comp_C
+ finSuccEquiv_renameEquiv_finSuccEquiv
+ image_product_antidiagonal_optionElim
+ isEmptyEquiv
+ iterToSum
+ iterToSumFun
+ iterToSumFun_C_X
+ iterToSumFun_X
+ iterToSum_C_C
+ iterToSum_apply
+ mapAlgEquiv
+ mapAlgEquiv_refl
+ mapAlgEquiv_symm
+ mapAlgEquiv_trans
+ mapEquiv
+ mapEquiv_refl
+ mapEquiv_symm
+ mapEquiv_trans
+ map_injective
+ map_injective_iff
+ map_leftInverse
+ map_rightInverse
+ map_surjective
+ map_surjective_iff
+ optionEquivLeft
+ optionEquivLeft_C
+ optionEquivLeft_X_none
+ optionEquivLeft_X_some
+ optionEquivLeft_monomial
+ optionEquivRight
+ optionEquivRight_C
+ optionEquivRight_X_none
+ optionEquivRight_X_some
+ optionEquivRight_monomial
+ optionFunLeft
+ optionFunLeft_monomial
+ optionFunLeft_mul
+ optionFunRight
+ optionFunRight_monomial
+ optionFunRight_mul
+ optionInvFunLeft
+ optionInvFunRight
+ sumAlgEquiv
+ sumAlgEquiv_comp_rename_inl
+ sumAlgEquiv_comp_rename_inr
+ sumToIter
+ sumToIterFun
+ sumToIterFun_monomial
+ sumToIterFun_mul
+ sumToIter_C
+ sumToIter_Xl
+ sumToIter_Xr
+ sumToIter_monomial
+ uniqueEquiv
+ uniqueEquiv_C
+ uniqueEquiv_X

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
6896	1	backward.isDefEq

Current commit 3a4144f03d
Reference commit b301d257a1

You can run this locally as

./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(Data/Finsupp): add computational lemmas for cons and single #35329
• [Merged by Bors] - feat(Data/Finsupp): add lemmas for Finsupp and Sum #36506
  By Dependent Issues (🤖). Happy coding!