Commit 2026-09-30 15:24 45f06029
View on Github →chore: complete generalization of oneLePart lemmas to DivInvMonoid (#41584)
This PR completes the generalization of Mathlib/Algebra/Order/Group/PosPart.lean started by #41247
It weakens the hypotheses of the form Group α to DivInvOneMonoid α in numerous results, thus allowing them to apply to EReal (the motivation).