Mathlib v3 is deprecated. Go to Mathlib v4

Def with_bot.gi_unbot'_bot

Modification history

2022-10-24 01:07

src/order/galois_connection.lean

refactor(data/polynomial/degree): use `with_bot.unbot'` instead of `option.get_or_else` (#17120)

Added with_bot.gi_unbot'_bot View on Github →