shake

leanprover-community · Sep 11, 2024 · 9405e9a · 9405e9a
1 parent 42050b8
commit 9405e9a
Show file tree

Hide file tree

Showing 5 changed files with 1 addition and 4 deletions.
diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Int.Cast.Defs
-import Mathlib.Algebra.NeZero
 import Mathlib.Logic.Function.Basic
 
 /-!

diff --git a/Mathlib/Algebra/Order/ZeroLEOne.lean b/Mathlib/Algebra/Order/ZeroLEOne.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import Mathlib.Order.Basic
-import Mathlib.Algebra.NeZero
 
 /-!
 # Typeclass expressing `0 ≤ 1`.

diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
@@ -9,6 +9,7 @@ import Mathlib.Algebra.Ring.Nat
 import Mathlib.Order.Basic
 import Mathlib.Tactic.AdaptationNote
 import Mathlib.Tactic.Common
+import Mathlib.Algebra.NeZero
 
 /-!
 # Bitwise operations on natural numbers

diff --git a/Mathlib/Data/Nat/Cast/NeZero.lean b/Mathlib/Data/Nat/Cast/NeZero.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Mathlib.Data.Nat.Cast.Defs
-import Mathlib.Algebra.NeZero
 
 /-!
 # Lemmas about nonzero elements of an `AddMonoidWithOne`

diff --git a/Mathlib/Data/PNat/Defs.lean b/Mathlib/Data/PNat/Defs.lean
@@ -3,7 +3,6 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Neil Strickland
 -/
-import Mathlib.Algebra.NeZero
 import Mathlib.Data.Nat.Defs
 import Mathlib.Order.Basic
 import Mathlib.Order.TypeTags