split/rename PowerSeries/Basic ?

Stream: mathlib4

[Antoine Chambert-Loir]

The file containing docs#PowerSeries is huge and consists roughly of two parts:

• a general theory of power series in several variables (docs#MvPowerSeries)
• the particular case of one variable (docs#PowerSeries) defined as MvPowerSeries Unit
  I wonder whether it would be reasonable to have the first part in RingTheory/MvPowerSeries, and the second one staying there.

A possibly more interesting TODO would be to define the large algebra of an additive monoid when the addition of this monoid has finite fibers. (docs#MvPowerSeries would be a particular case of that for the monoid I to_0 Nat.)
(In this case, power series appear as a particular case of docs#HahnSeries, but I haven't thought about whether the two generalizations are comparable or not.)

[Antoine Chambert-Loir]

By the way, docs#Polynomial is not defined as a particular case of docs#MvPolynomial, so this raises the question whether both theories could be developed in parallel.

[Johan Commelin]

Your proposed split seems fine to me.
I don't have an opinion on the refactor.

[Eric Wieser]

The power/mvpower split sounds very sensible to me