Theorem oneLePart_mono

Modification history

2024-10-16 02:20

Mathlib/Algebra/Order/Group/PosPart.lean

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

Modified oneLePart_mono View on Github →

2024-01-16 16:52

Mathlib/Algebra/Order/Group/PosPart.lean

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

Added oneLePart_mono View on Github →