Theorem PowerSeries.order_pow

Modification history

2025-11-07 10:29
Mathlib/RingTheory/PowerSeries/Order.lean
feat(RingTheory/PowerSeries/Order): PowerSeries.divXPowOrder_pow (#31331) …
Modified PowerSeries.order_powView on Github →
2025-04-16 15:35
Mathlib/RingTheory/PowerSeries/Order.lean
feat (RingTheory/PowerSeries/Order) : compute order of power and generalize (#23993) …
Added PowerSeries.order_powView on Github →