Commit 2025-11-07 10:29 c92d3381

View on Github →

feat(RingTheory/PowerSeries/Order): PowerSeries.divXPowOrder_pow (#31331)

  • Deprecate divXPowOrder_mul_divXPowerOrder in favour of divXPowOrder_mul (the same equality in reverse, the conventional direction for monoid homs)
  • Define MonoidHom versions of order and divXPowOrder and use them to prove order_pow and order_prod, divXPowOrder_pow and divXPowOrder_prod (in a nontrivial semiring with no zero divisors).

Estimated changes

modified theorem PowerSeries.order_pow