Skip to content

Commit

Permalink
chore: Delete Data.Int.Dvd.Pow (#12823)
Browse files Browse the repository at this point in the history
These three lemmas are oddly stated and completely unused in mathlib.
  • Loading branch information
YaelDillies committed May 13, 2024
1 parent de05555 commit 281655a
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 40 deletions.
1 change: 0 additions & 1 deletion Mathlib.lean
Expand Up @@ -1913,7 +1913,6 @@ import Mathlib.Data.Int.ConditionallyCompleteOrder
import Mathlib.Data.Int.Defs
import Mathlib.Data.Int.Div
import Mathlib.Data.Int.Dvd.Basic
import Mathlib.Data.Int.Dvd.Pow
import Mathlib.Data.Int.GCD
import Mathlib.Data.Int.Interval
import Mathlib.Data.Int.LeastGreatest
Expand Down
39 changes: 0 additions & 39 deletions Mathlib/Data/Int/Dvd/Pow.lean

This file was deleted.

0 comments on commit 281655a

Please sign in to comment.