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?

Estimated changes