mathlib

b2b39edd - chore(order/galois_connection): define `with_bot.gi_get_or_else_bot` (#4781)

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`.