MvPowerSeries - huge file

Stream: mathlib4

[Antoine Chambert-Loir]

For the moment, Mathlib/MvPowerSeries/Basic.lean is a huge file with ~ 3k lines.
To start with, what about splitting it in two files,

• Mathlib/MvPowerSeries/Basic.lean : first 1300 lines
• Mathlib/PowerSeries/Basic.lean : everything about power series in one variable (the 2600 remaining lines)

If one wishes to split them in more files,
for docs#MvPowerSeries :

• one could take out the trunc section to …/Trunc.lean
• and everything about inverses, and the local ring property to …/Inverse.lean

and for docs#PowerSeries :

• trunc to …/Trunc.lean
• everything about inverses to …/Inverse.lean
• everything about order to …/Order.lean

[Antoine Chambert-Loir]

I take these three thumbs as an encouragement to do that. Tomorrow, if everything is ok.

[Antoine Chambert-Loir]

#10866

[Kevin Buzzard]

My memory of mvpolynomials was that at some point in the past people could import the Basic file and then multiplication or subtraction (I can't remember which) wouldn't work because you needed to import the Ring file as well. People found this very confusing. It would be good if the Basic mvpowerseries file still has enough in it to make the basics work!

[Riccardo Brasca]

It looks like a very good change to me.

[Antoine Chambert-Loir]

In fact, only a few files do import power series.
They used to import PowerSeries.Basic, and that still suffices for most of them, although I didn't check whether MvPowerSeries.Basic would have sufficed. (The “import” linter didn't complain in this direction.) For one or two files, Inversewas required. I don't think Trunc or Order had to be imported.

[Yaël Dillies]

Order sounds like an uncontroversial thing to split out. I don't know about the rest