Commit 2025-09-30 09:47 12016cb0

View on Github →

feat(RingTheory): (Mv)PowerSeries.(weighted)Order of neg (#29760) Also renamed the wrong PowerSeries.order_add_of_order_eq while I am at it.

Estimated changes

Modified Mathlib/RingTheory/MvPowerSeries/Order.lean

added theorem MvPowerSeries.order_neg

added theorem MvPowerSeries.weightedOrder_neg

Modified Mathlib/RingTheory/PowerSeries/Order.lean

deleted theorem PowerSeries.order_add_of_order_eq

added theorem PowerSeries.order_add_of_order_ne

added theorem PowerSeries.order_neg