Commit 2025-05-13 08:28 02706e7c

View on Github →

chore: remove CanonicallyOrdered{Mul, Add}.toOrderBot (#24094) This will allow us to use CanonicallyOrdered{Mul, Add} with order typeclasses that extend Bot.

Estimated changes

modified theorem bot_eq_one'
modified theorem bot_eq_one
modified theorem eq_one_or_one_lt
added theorem isBot_one
modified theorem le_one_iff_eq_one
modified theorem one_lt_iff_ne_one
modified theorem one_lt_of_ne_one
modified theorem one_not_mem_iff
modified theorem Nat.cast_finsetSup
modified theorem Order.succ_eq_zero