Commit 2025-05-14 10:34 37c01f2e

View on Github →

feat(RingTheory/PowerSeries/Substitution): define substitution of power series in power series (#23552) This is the second part of the PR defining substitution of indeterminates by power series in power series. This one is specific to univariate power series. Basically, the matter is just to remove Unit -> in definitions and make the necessary adjustments.

Estimated changes

modified theorem PowerSeries.aeval_coe
modified theorem PowerSeries.aeval_eq_sum
modified theorem PowerSeries.coe_aeval
modified theorem PowerSeries.coe_eval₂Hom
modified theorem PowerSeries.comp_aeval
modified theorem PowerSeries.comp_eval₂
modified theorem PowerSeries.eval₂_eq_tsum
modified theorem PowerSeries.eval₂_unique
modified theorem PowerSeries.hasSum_aeval
modified theorem PowerSeries.hasSum_eval₂
added theorem PowerSeries.subst_X
added theorem PowerSeries.subst_add
added theorem PowerSeries.subst_coe
added theorem PowerSeries.subst_mul
added theorem PowerSeries.subst_pow
added theorem PowerSeries.subst_smul