Commit 2025-04-02 07:08 04b72bc2
View on Github →feat(MvPowerSeries/Substitution): substitution of power series inside power series (#15158) Define substitution of power series other power series. This is an application of evaluation, where the ground ring is given the discrete topology. The condition for being defined is that the constant coefficient is nilpotent (and, for infinitely many variables, that the family tends to 0).