Commit 2022-12-17 23:54 da4d01da
View on Github →feat: port Data.Int.Dvd.Pow (#1087)
mathlib SHA : b3f25363ae62cb169e72cd6b8b1ac97bacf21ca7
I don't know what to do with sign_pow_bit1
. I get a warning that bit1
is deprecated, does that mean I should just delete the lemma?