Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-11-20 08:25
55c020e1
View on Github →
feat(Order/WithBot): Equiv.withBotSubtypeNe (
#19251
) Needed in
#19210
From the Carleson project
Estimated changes
Modified
Mathlib/Order/WithBot.lean
added
def
Equiv.withBotSubtypeNe
added
def
Equiv.withTopSubtypeNe