Theorem oneLePart_max

Modification history

2025-10-23 17:08

Mathlib/Algebra/Order/Group/PosPart.lean

feat: interplay of posPart, negPart, untop₀, min and max (#30774) …

Added oneLePart_max View on Github →