Commit 2025-10-25 20:23 1ab7b2e0

View on Github →

chore: rephrase leOnePart_le_one/negPart_nonpos (#30899) The current phrasing is identical to that of the primed lemmas.

Estimated changes

modified theorem leOnePart_le_one