Commit 2023-09-25 13:30 b915222e

View on Github →

feat(Order/WithBot): add some lemmas (#6275) The WithTop version of the last 3 lemmas already exists.

Estimated changes

Modified Mathlib/Data/Polynomial/Degree/Definitions.lean

Modified Mathlib/Order/GaloisConnection.lean

Modified Mathlib/Order/WithBot.lean

deleted theorem WithBot.unbot'_bot_le_iff

added theorem WithBot.unbot'_le_iff

modified theorem WithBot.unbot'_lt_iff

added theorem WithTop.coe_untop'_le

added theorem WithTop.le_untop'_iff

added theorem WithTop.lt_untop'_iff