split power series in several files (#10866)

This PR split the files devoted to power series (especially RingTheory/PowerSeries/Basic) into several ones:

* RingTheory/MvPowerSeries/Basic - initial definitions (multivariate)
* RingTheory/MvPowerSeries/Trunc - truncation
* RingTheory/MvPowerSeries/Inverse - stuff pertaining to inverses

* RingTheory/PowerSeries/Basic - initial definitions (univariate)
* RingTheory/PowerSeries/Trunc - truncation
* RingTheory/PowerSeries/Inverse - stuff pertaining to inverses
* RingTheory/PowerSeries/Order - stuff pertaining to order

it remains to adjust the other files (PowerSeries/Derivative and PowerSeries/WellKnown)



Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: faenuccio <filippo.nuccio@univ-st-etienne.fr>

Archive/Wiedijk100Theorems/Partition.lean

@@ -3,7 +3,8 @@ Copyright (c) 2020 Bhavik Mehta, Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Aaron Anderson
 -/
-import Mathlib.RingTheory.PowerSeries.Basic
+import Mathlib.RingTheory.PowerSeries.Inverse
+import Mathlib.RingTheory.PowerSeries.Order
 import Mathlib.Combinatorics.Partition
 import Mathlib.Data.Nat.Parity
 import Mathlib.Data.Finset.NatAntidiagonal

Mathlib.lean

@@ -3308,6 +3308,9 @@ import Mathlib.RingTheory.MvPolynomial.NewtonIdentities
 import Mathlib.RingTheory.MvPolynomial.Symmetric
 import Mathlib.RingTheory.MvPolynomial.Tower
 import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
+import Mathlib.RingTheory.MvPowerSeries.Basic
+import Mathlib.RingTheory.MvPowerSeries.Inverse
+import Mathlib.RingTheory.MvPowerSeries.Trunc
 import Mathlib.RingTheory.Nakayama
 import Mathlib.RingTheory.Nilpotent
 import Mathlib.RingTheory.Noetherian
@@ -3349,6 +3352,9 @@ import Mathlib.RingTheory.PolynomialAlgebra
 import Mathlib.RingTheory.PowerBasis
 import Mathlib.RingTheory.PowerSeries.Basic
 import Mathlib.RingTheory.PowerSeries.Derivative
+import Mathlib.RingTheory.PowerSeries.Inverse
+import Mathlib.RingTheory.PowerSeries.Order
+import Mathlib.RingTheory.PowerSeries.Trunc
 import Mathlib.RingTheory.PowerSeries.WellKnown
 import Mathlib.RingTheory.Prime
 import Mathlib.RingTheory.PrincipalIdealDomain

Mathlib/NumberTheory/Bernoulli.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin, Kevin Buzzard
 import Mathlib.Algebra.BigOperators.NatAntidiagonal
 import Mathlib.Algebra.GeomSum
 import Mathlib.Data.Fintype.BigOperators
+import Mathlib.RingTheory.PowerSeries.Inverse
 import Mathlib.RingTheory.PowerSeries.WellKnown
 import Mathlib.Tactic.FieldSimp