Commit 2025-12-18 09:08 86622378

View on Github →

feat(RingTheory/MvPowerSeries): some APIs about expand (#33005) I define an algebraic homomorphism for (mv) power series that expanding a (multi) variate power series by a non-zero factor of p and add some theorems following the (mv) Polynomial as inspiration. Also, I add some missing theorems in the file MvPolynomial.Expand compared to Polynomial.Expand.

Estimated changes

modified theorem MvPolynomial.eval_expand
modified theorem MvPolynomial.eval₂_expand
modified theorem MvPolynomial.expand_C
modified theorem MvPolynomial.expand_X
modified theorem MvPolynomial.expand_bind₁
modified theorem MvPolynomial.expand_mul
modified theorem MvPolynomial.map_expand
modified theorem MvPolynomial.rename_expand
modified theorem MvPolynomial.support_expand
added theorem MvPowerSeries.expand_C
added theorem MvPowerSeries.expand_X
added theorem PowerSeries.expand_C
added theorem PowerSeries.expand_X
added theorem PowerSeries.expand_mul
added theorem PowerSeries.expand_one
added theorem PowerSeries.map_expand
added theorem PowerSeries.map_subst