Mathlib Changelog
v4
Changelog
About
Github
Theorem
one_lt_leOnePart_iff
Modification history
2025-10-26 09:23
Mathlib/Algebra/Order/Group/PosPart.lean
chore: rename lemmas with 'ltOnePart' in their name (#30903) …
Added
one_lt_leOnePart_iff
View on Github →