Commit 2024-05-13 15:49 281655a9

View on Github →

chore: Delete Data.Int.Dvd.Pow (#12823) These three lemmas are oddly stated and completely unused in mathlib.

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Data/Int/Dvd/Pow.lean

deleted theorem Int.dvd_of_pow_dvd

deleted theorem Int.pow_dvd_of_le_of_pow_dvd

deleted theorem Int.sign_pow_bit1