refactor: change definition of restricted power series to align with restricted multivariate power series

[WilliamCoram]

Previously, restricted power series were defined in terms of a tendsto atTop this has been changed to be an abbrev of MvPowerSeries.IsRestricted with isRestricted_iff lemmas to convert to nicer usable definitions.

---

• depends on: [Merged by Bors] - feat: define multivariate restricted power series #32692

[github-actions]

PR summary e239c1e0ed

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.PowerSeries.Restricted	1695	1582	-113 (-6.67%)

Import changes for all files

Files	Import difference
Mathlib.RingTheory.PowerSeries.Restricted	-113

---

Declarations diff (regex)

+ addSubgroup
+ isRestricted.add
+ isRestricted.mul
+ isRestricted.neg
+ isRestricted_C
+ isRestricted_abs_iff
+ isRestricted_comp_uniqueEquiv
+ isRestricted_iff'
+ isRestricted_monomial
+ isRestricted_one
+ isRestricted_zero
+ subring
- C
- add
- convergenceSet
- convergenceSet_BddAbove
- isRestricted_iff_abs
- monomial
- mul
- neg
- one
- smul
- zero

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

• +12 new declarations
• −12 removed declarations

-PowerSeries.IsRestricted.C
-PowerSeries.IsRestricted.add
+PowerSeries.IsRestricted.addSubgroup
-PowerSeries.IsRestricted.convergenceSet
-PowerSeries.IsRestricted.convergenceSet_BddAbove
-PowerSeries.IsRestricted.isRestricted_iff
-PowerSeries.IsRestricted.isRestricted_iff_abs
-PowerSeries.IsRestricted.monomial
-PowerSeries.IsRestricted.mul
-PowerSeries.IsRestricted.neg
-PowerSeries.IsRestricted.one
-PowerSeries.IsRestricted.smul
+PowerSeries.IsRestricted.subring
-PowerSeries.IsRestricted.zero
+PowerSeries.isRestricted.add
+PowerSeries.isRestricted.mul
+PowerSeries.isRestricted.neg
+PowerSeries.isRestricted_C
+PowerSeries.isRestricted_abs_iff
+PowerSeries.isRestricted_iff
+PowerSeries.isRestricted_iff'
+PowerSeries.isRestricted_monomial
+PowerSeries.isRestricted_one
+PowerSeries.isRestricted_zero

---

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

Current number	Change	Type (strong)
391	-1	adaptation notes

No changes to weak technical debt.

Current commit e239c1e0ed
Reference commit 5f6fd26f8a

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-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: define multivariate restricted power series #32692
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[riccardobrasca]

Suggested change

	exact ⟨fun H => (H.comp (Finsupp.uniqueEquiv ()).symm.injective.tendsto_cofinite).congr fun n =>
	exact ⟨fun H ↦ (H.comp (Finsupp.uniqueEquiv ()).symm.injective.tendsto_cofinite).congr fun n ↦

Can you check this everywhere?

[riccardobrasca]

Suggested change

	variable {R : Type*} [NormedRing R]
	variable {R : Type*} [NormedRing R] (c : ℝ) (f : PowerSeries R)

Then you can remove it everywhere else.

[riccardobrasca]

I am not 100% it works, but can you to use MvPowerSeries.IsRestricted.addSubgroup directly?

[riccardobrasca]

Same as above.