Theorem MvPowerSeries.order_neg

Modification history

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