Skip to content

Commit 2f4c252

Browse files
committed
chore: reduce imports in several files (#14919)
Found by using the output of #14840.
1 parent 3bc3bfb commit 2f4c252

File tree

8 files changed

+0
-11
lines changed

8 files changed

+0
-11
lines changed

Mathlib/Algebra/Group/Action/Defs.lean

-2
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,6 @@ import Mathlib.Algebra.Group.Commute.Defs
77
import Mathlib.Algebra.Group.TypeTags
88
import Mathlib.Algebra.Opposites
99
import Mathlib.Logic.Embedding.Basic
10-
import Mathlib.Logic.Function.Iterate
11-
import Mathlib.Tactic.Common
1210

1311
/-!
1412
# Definitions of group actions

Mathlib/Algebra/GroupWithZero/WithZero.lean

-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro, Johan Commelin
55
-/
6-
import Mathlib.Algebra.Group.Equiv.Basic
76
import Mathlib.Algebra.Group.WithOne.Defs
87
import Mathlib.Algebra.GroupWithZero.Hom
98
import Mathlib.Algebra.GroupWithZero.Units.Basic

Mathlib/Algebra/Order/Interval/Set/Group.lean

-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot, Yury Kudryashov, Rémy
55
-/
66
import Mathlib.Algebra.Order.Group.Abs
77
import Mathlib.Algebra.Order.Group.Basic
8-
import Mathlib.Algebra.Order.Group.OrderIso
98
import Mathlib.Algebra.Order.Ring.Defs
109
import Mathlib.Data.Int.Cast.Lemmas
1110
import Mathlib.Order.Interval.Set.Basic

Mathlib/Data/Int/Cast/Lemmas.lean

-2
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,6 @@ Authors: Mario Carneiro
55
-/
66
import Mathlib.Algebra.Ring.Hom.Basic
77
import Mathlib.Algebra.Ring.Int
8-
import Mathlib.Data.Nat.Cast.Basic
9-
import Mathlib.Data.Nat.Cast.Commute
108

119
/-!
1210
# Cast of integers (additional theorems)

Mathlib/Data/Nat/Cast/Basic.lean

-2
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
66
import Mathlib.Algebra.Divisibility.Basic
7-
import Mathlib.Algebra.Group.Equiv.Basic
8-
import Mathlib.Algebra.Group.TypeTags
97
import Mathlib.Algebra.Ring.Hom.Defs
108
import Mathlib.Algebra.Ring.Nat
119

Mathlib/Data/Nat/Cast/Order/Basic.lean

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
66
import Mathlib.Data.Nat.Cast.Basic
7-
import Mathlib.Algebra.CharZero.Defs
87
import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
98
import Mathlib.Data.Nat.Cast.NeZero
109
import Mathlib.Algebra.Order.ZeroLEOne

Mathlib/Data/Set/Pairwise/Basic.lean

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl
55
-/
66
import Mathlib.Data.Set.Function
7-
import Mathlib.Logic.Relation
87
import Mathlib.Logic.Pairwise
98

109
/-!

Mathlib/Tactic/CategoryTheory/Reassoc.lean

-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Scott Morrison
55
-/
66
import Mathlib.CategoryTheory.Functor.Basic
77
import Mathlib.Util.AddRelatedDecl
8-
import Mathlib.Lean.Meta.Simp
98

109
/-!
1110
# The `reassoc` attribute

0 commit comments

Comments
 (0)