Commit 2024-06-10 07:27 38962a38
View on Github →chore(*): drop some bit0/bit1 lemmas (#13679)
Since bit0
and bit1
are deprecated in Lean 4, these lemmas were deprecated for a long time.
Also move Filter.nonneg_of_eventually_pow_nonneg
to Order/Filter/ModEq
.