Theorem oneLePart_def

Modification history

2024-10-16 02:20
Mathlib/Algebra/Order/Group/PosPart.lean
refactor: turn `posPart` into a notation class again (#17426)
Added oneLePart_defView on Github →