diff --git a/Mathlib/Algebra/CharZero/Defs.lean b/Mathlib/Algebra/CharZero/Defs.lean index 8f2cf74d4cef2..c82356e6fa6e7 100644 --- 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 index ecd0e356d73ad..538c8f6985b42 100644 --- 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 index d04abc89e9c53..d57eb4da599b5 100644 --- 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 index d49f78b3b3095..c3f00eb8b8820 100644 --- 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 index 3004d33fc9df7..6eb644184ac56 100644 --- 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