Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-19 21:48
260650d9
View on Github →
feat(Order/OrderIsoNat): sequence in well-founded order is not
StrictAnti
(
#20851
)
Estimated changes
Modified
Mathlib/Order/OrderIsoNat.lean
added
theorem
not_strictAnti_of_wellFoundedLT
added
theorem
not_strictMono_of_wellFoundedGT