Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-14 10:46
b2b616a6
View on Github →
feat(Algebra/Order/SuccPred):
¬ IsSuccLimit n
for
n : ℕ
(
#21855
)
Estimated changes
Modified
Mathlib/Algebra/Order/SuccPred.lean
added
theorem
Order.IsSuccLimit.natCast_lt
added
theorem
Order.not_isSuccLimit_natCast