Theorem PowerSeries.order_neg

Modification history

2025-09-30 09:47
Mathlib/RingTheory/PowerSeries/Order.lean
feat(RingTheory): (Mv)PowerSeries.(weighted)Order of neg (#29760) …
Added PowerSeries.order_negView on Github →