Commit 2024-10-27 12:33 1a0cb23b

View on Github →

chore(RingTheory/PowerSeries/Basic): rename Polynomial.ToPowerSeries -> Polynomial.toPowerSeries (#18265) According to naming convention, it should be Polynomial.toPowerSeries. It's already MvPolynomial.toMvPowerSeries for MvPolynomial.

Estimated changes