Skip to content

Commit d682465

Browse files
committed
chore: update lean + std4 09-05 (#401)
1 parent 74e0984 commit d682465

File tree

21 files changed

+40
-1759
lines changed

21 files changed

+40
-1759
lines changed

Mathlib.lean

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ import Mathlib.Data.UnionFind
2828
import Mathlib.Init.Algebra.Functions
2929
import Mathlib.Init.Algebra.Order
3030
import Mathlib.Init.Data.Int.Basic
31-
import Mathlib.Init.Data.Int.Order
31+
import Mathlib.Init.Data.Int.Notation
3232
import Mathlib.Init.Data.List.Basic
3333
import Mathlib.Init.Data.List.Instances
3434
import Mathlib.Init.Data.List.Lemmas
@@ -83,9 +83,6 @@ import Mathlib.Tactic.IrreducibleDef
8383
import Mathlib.Tactic.LeftRight
8484
import Mathlib.Tactic.LibrarySearch
8585
import Mathlib.Tactic.NormCast
86-
import Mathlib.Tactic.NormCast.CoeExt
87-
import Mathlib.Tactic.NormCast.Ext
88-
import Mathlib.Tactic.NormCast.Lemmas
8986
import Mathlib.Tactic.NormCast.Tactic
9087
import Mathlib.Tactic.NormNum
9188
import Mathlib.Tactic.PermuteGoals

Mathlib/Algebra/Group/Defs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import Mathlib.Init.Data.Nat.Lemmas
2-
import Mathlib.Init.Data.Int.Basic
2+
import Mathlib.Init.Data.Int.Notation
33
import Mathlib.Init.Zero
44
import Mathlib.Tactic.Spread
55
import Mathlib.Tactic.ToAdditive

Mathlib/Algebra/Ring/Basic.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
import Mathlib.Init.Data.Int.Basic
21
import Mathlib.Algebra.GroupWithZero.Defs
32
import Mathlib.Algebra.Group.Basic
43
import Mathlib.Tactic.Spread

Mathlib/Control/Random.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Henrik Böving
55
-/
66
import Mathlib.Init.Algebra.Order
77
import Mathlib.Init.Data.Nat.Lemmas
8-
import Mathlib.Init.Data.Int.Order
8+
import Mathlib.Init.Data.Int.Basic
99
import Mathlib.Data.Fin.Basic
1010
import Mathlib.Data.Nat.Basic
1111

0 commit comments

Comments
 (0)