Commit 2025-04-18 12:43 ec24b5f9

chore: use order of power series to prove NoZeroDivisors (#24152) This is the approach used in the multivariate case, and the current proof is essentially a hand-made version of the order argument. This means moving all the results depending on this in a new file depending on PowerSeries.Order, which I call PowerSeries.NoZeroDivisors (analogous to the existing MvPowerSeries.NoZeroDivisors). Also do a little bit of cleanup in the proof of order_mul using the cleanup from #24072. This is a followup to #23993 and #24072.