Work on MvPowerSeries

Stream: PR reviews

[Antoine Chambert-Loir]

@María Inés de Frutos Fernández and I are uploading a series of PRs regarding docs#MvPowerSeries, providing order, lexicographic order, evaluation and substitution.

This message is to record them and (hopefully) help potential reviewers through them.

• #14865. Coefficients of $f ^ m$, for some power series $f$.

• #14866. Defines the “natural” topology on MvPowerSeries, aka the topology of simple convergence on the coefficients, aka the product topology. Because some other topologies are useful too, it is only introduced as scoped instance WithPiTopology. (Maybe that new file should be called PiTopology.lean.) This topology is Hausdorff and complete if so is the ring of coefficients.
  (Note that the topology is generally not the adic topology.)

• #14981 : Lexicographic order for multivariate power series, and the fact that they form a domain if the semiring of coefficients does.

• #14983 : order of multivariate power series. (Before that, it only existed for PowerSeries.) (The various indeterminates need not have the same weight.)

• #14989 : A multivariate power series is the sum of its “homogeneous” components.

• #14990 : definition of the classLinearTopology that asserts that the topology of a ring has a basis of neighborhoods of 0 consisting of ideals.

• #15007 : the “PiTopology” on multivariate power series is a linear topology

• #15019 : evaluation of multivariate power series in complete Hausdorff topological algebras with a linear topology.
  This PR also introduces the notion of a topological algebra, and a variant of docs#MvPowerSeries.trunc of MvPowerSeries (with large inequality instead of strict).

• #15158 : substitution of power series inside power series (under the condition that the constant coefficient is nilpotent and, if there are infinitely many variables, that the series to be substituted converge to zero).

[Johan Commelin]

I left some comments on the first half.

[María Inés de Frutos Fernández]

Thanks to everyone who reviewed these! #14866, #14981 and #14983 are again ready for review (and blocking some of the following ones).