Commit 2026-08-19 10:07 35b2c4c1

View on Github →

fix(RingTheory/PowerSeries): rename order_zero_of_unit to order_zero_of_isUnit (#42930)

Estimated changes

Modified Mathlib/RingTheory/PowerSeries/Exp.lean

Modified Mathlib/RingTheory/PowerSeries/Inverse.lean

Modified Mathlib/RingTheory/PowerSeries/Order.lean

added theorem PowerSeries.order_zero_of_isUnit

deleted theorem PowerSeries.order_zero_of_unit