Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-24 01:07 a15401cf

View on Github →

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

Estimated changes

modified def polynomial.nat_degree
deleted theorem with_bot.get_or_else_bot
added theorem with_bot.le_coe_unbot'
added theorem with_bot.unbot'_lt_iff