Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-08-07 16:33
a88cdb66
View on Github →
feat(RelSeries): head_singleton, last_singleton (
#15384
) from the Carleson project.
Estimated changes
Modified
Mathlib/Order/RelSeries.lean
added
theorem
RelSeries.head_singleton
added
theorem
RelSeries.last_singleton