Commit 2026-07-02 15:44 05742115
View on Github →chore: generalize instPosPart to SubNegMonoid (#41247)
This PR generalizes the OneLePart and LeOnePart instances to DivInvMonoid instead of Group, and similarly for their additive versions.
My goal is to have PosPart for EReal.