Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-22 15:16 79ac4c81

View on Github →

chore(data/polynomial/degree/definitions): simplify sum_fin, degree_C_le (#13564)

Estimated changes

Modified src/data/polynomial/degree/definitions.lean

added theorem polynomial.nat_degree_lt_iff_degree_lt

Modified src/order/bounded_order.lean

added theorem with_bot.get_or_else_bot_lt_iff