Def oneLePart

Modification history

2024-10-16 02:20

Mathlib/Algebra/Order/Group/PosPart.lean

refactor: turn `posPart` into a notation class again (#17426)

Deleted oneLePart View on Github →

2024-01-16 16:52

Mathlib/Algebra/Order/Group/PosPart.lean

refactor: Clean up `posPart` (#9740) …

Added oneLePart View on Github →