Commit 2020-10-26 05:21 b2b39edd

View on Github →

chore(order/galois_connection): define with_bot.gi_get_or_else_bot (#4781) This Galois insertion can be used to golf proofs about polynomial.degree vs polynomial.nat_degree.

Estimated changes

Modified src/data/option/basic.lean

added theorem option.get_or_else_coe

Modified src/order/bounded_lattice.lean

added theorem with_bot.get_or_else_bot

added theorem with_bot.get_or_else_bot_le_iff

Modified src/order/galois_connection.lean

added def with_bot.gi_get_or_else_bot