Theorem oneLePart_one

Modification history

2024-10-18 09:18

Mathlib/Algebra/Order/Group/PosPart.lean

chore(PosPart): Make more lemmas simp (#17053)

Modified oneLePart_one View on Github →

2024-03-07 15:09

Mathlib/Algebra/Order/Group/PosPart.lean

chore(Order): Make more arguments explicit (#11033) …

Modified oneLePart_one View on Github →

2024-01-16 16:52

Mathlib/Algebra/Order/Group/PosPart.lean

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

Added oneLePart_one View on Github →