Theorem PowerSeries.order_add_of_order_ne

Modification history

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