Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-09-17 16:23
58f26a02
View on Github →
chore(order/bounded_lattice): trivial generalizations (
#9246
)
Estimated changes
Modified
src/order/bounded_lattice.lean
modified
theorem
with_bot.coe_le
modified
theorem
with_bot.coe_lt_coe
modified
theorem
with_top.coe_le_coe
modified
theorem
with_top.coe_lt_coe
modified
theorem
with_top.coe_lt_iff
modified
theorem
with_top.coe_lt_top
modified
theorem
with_top.le_coe
modified
theorem
with_top.not_top_le_coe