feat(RingTheory.MvPowerSeries.Topology): define the product topology on mv power series

[AntoineChambert-Loir]

Let R be with Semiring R and TopologicalSpace R
In this file we define the topology on MvPowerSeries σ R
that corresponds to the simple convergence on its coefficients,
aka the product topology.
It is the coarsest topology for which all coefficients maps are continuous.

When R has UniformSpace R, we define the corresponding uniform structure.

When the type of coefficients has the discrete topology,
it corresponds to the topology defined by [bourbaki1981], chapter 4, §4, n°2

Coauthored with María Inés de Frutos Fernández @mariainesdff

---

• depends on: [Merged by Bors] - feat(MvPowerSeries.Basic): compute coefficients of powers of MvPowerSeries #14865
  

[github-actions]

PR summary 57fce93dad

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.MvPowerSeries.PiTopology	1079
Mathlib.RingTheory.PowerSeries.PiTopology	1102

---

Declarations diff

+ MvPowerSeries.apply_eq_coeff
+ prod_one_add
+ variables_tendsto_zero
++ as_tsum
++ continuous_C
++ continuous_coeff
++ continuous_constantCoeff
++ hasSum_of_monomials_self
++ instCompleteSpace
++ instT0Space
++ instT2Space
++ instTopologicalRing
++ instTopologicalSemiring
++ instUniformAddGroup
++ tendsto_iff_coeff_tendsto
++ tendsto_pow_of_constantCoeff_nilpotent_iff
++ tendsto_pow_zero_of_constantCoeff_nilpotent
++ tendsto_pow_zero_of_constantCoeff_zero
++ uniformContinuous_coeff

You can run this locally as follows

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

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

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

[loefflerd]

Should this go elsewhere?

[loefflerd]

This can probably be shortened using dot-notation

[YaelDillies]

Good idea to have both files in the same PR. I get to write twice as few comments 😁

[YaelDillies]

Suggested change

	(s.prod fun i => 1 + f i) = s.powerset.sum fun t => t.prod f := by
	∏ i ∈ s, (1 + f i) = ∑ t ∈ s.powerset, t.prod f := by

[YaelDillies]

Suggested change

	/-- coeff are continuous -/
	/-- `MvPowerSeries.coeff` is continuous. -/

[YaelDillies]

Could you try using fun_prop here?

[YaelDillies]

Suggested change

	theorem continuous_coeff [Semiring R] (d : σ →₀ ℕ) : Continuous (MvPowerSeries.coeff R d) :=
	@[fun_prop]
	theorem continuous_coeff [Semiring R] (d : σ →₀ ℕ) : Continuous (MvPowerSeries.coeff R d) :=

[YaelDillies]

Suggested change

	theorem continuous_C [Ring R] [TopologicalRing R] :
	@[fun_prop]
	theorem continuous_C [Ring R] [TopologicalRing R] :