Commit 2025-10-26 09:23 841fd68d

View on Github →

chore: rename lemmas with 'ltOnePart' in their name (#30903) There's no such thing as ltOnePart; they're referring to leOnePart.

Estimated changes

added theorem one_lt_leOnePart
added theorem one_lt_leOnePart_iff
deleted theorem one_lt_ltOnePart
deleted theorem one_lt_ltOnePart_iff