Skip to content

Commit 6a54a80

Browse files
kim-emKha
kim-em
and
Kha
committed
chore: move Mathlib to the module system (#31786)
This PR is a continuation of leanprover-community#80, but now targeting Mathlib `master` rather than `nightly-testing`. Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
1 parent 1e783fb commit 6a54a80

File tree

7,210 files changed

+58001
-29784
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

7,210 files changed

+58001
-29784
lines changed

‎.github/build.in.yml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ jobs:
3838
lint-outcome: ${{ steps.lint.outcome }}
3939
mk_all-outcome: ${{ steps.mk_all.outcome }}
4040
noisy-outcome: ${{ steps.noisy.outcome }}
41+
# shake-outcome: ${{ steps.shake.outcome }}
4142
test-outcome: ${{ steps.test.outcome }}
4243
defaults: # On Hoskinson runners, landrun is already installed.
4344
run: # note that .pr-branch/.lake must be created in a step below before we use this

‎.github/workflows/bors.yml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ jobs:
4848
lint-outcome: ${{ steps.lint.outcome }}
4949
mk_all-outcome: ${{ steps.mk_all.outcome }}
5050
noisy-outcome: ${{ steps.noisy.outcome }}
51+
# shake-outcome: ${{ steps.shake.outcome }}
5152
test-outcome: ${{ steps.test.outcome }}
5253
defaults: # On Hoskinson runners, landrun is already installed.
5354
run: # note that .pr-branch/.lake must be created in a step below before we use this

‎.github/workflows/build.yml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ jobs:
5555
lint-outcome: ${{ steps.lint.outcome }}
5656
mk_all-outcome: ${{ steps.mk_all.outcome }}
5757
noisy-outcome: ${{ steps.noisy.outcome }}
58+
# shake-outcome: ${{ steps.shake.outcome }}
5859
test-outcome: ${{ steps.test.outcome }}
5960
defaults: # On Hoskinson runners, landrun is already installed.
6061
run: # note that .pr-branch/.lake must be created in a step below before we use this

‎.github/workflows/build_fork.yml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@ jobs:
5252
lint-outcome: ${{ steps.lint.outcome }}
5353
mk_all-outcome: ${{ steps.mk_all.outcome }}
5454
noisy-outcome: ${{ steps.noisy.outcome }}
55+
# shake-outcome: ${{ steps.shake.outcome }}
5556
test-outcome: ${{ steps.test.outcome }}
5657
defaults: # On Hoskinson runners, landrun is already installed.
5758
run: # note that .pr-branch/.lake must be created in a step below before we use this

‎Mathlib.lean‎

Lines changed: 7209 additions & 7205 deletions
Large diffs are not rendered by default.

‎Mathlib/Algebra/AddConstMap/Basic.lean‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,12 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov
55
-/
6-
import Mathlib.Algebra.Group.Action.Pi
7-
import Mathlib.Algebra.Group.End
8-
import Mathlib.Algebra.Module.NatInt
9-
import Mathlib.Algebra.Order.Archimedean.Basic
6+
module
7+
8+
public import Mathlib.Algebra.Group.Action.Pi
9+
public import Mathlib.Algebra.Group.End
10+
public import Mathlib.Algebra.Module.NatInt
11+
public import Mathlib.Algebra.Order.Archimedean.Basic
1012

1113
/-!
1214
# Maps (semi)conjugating a shift to a shift
@@ -26,6 +28,8 @@ We use parameters `a` and `b` instead of `1` to accommodate for two use cases:
2628
including orientation-reversing maps.
2729
-/
2830

31+
@[expose] public section
32+
2933
assert_not_exists Finset
3034

3135
open Function Set

‎Mathlib/Algebra/AddConstMap/Equiv.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,9 @@ Copyright (c) 2024 Yury Kudryashov. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Yury Kudryashov
55
-/
6-
import Mathlib.Algebra.AddConstMap.Basic
6+
module
7+
8+
public import Mathlib.Algebra.AddConstMap.Basic
79

810
/-!
911
# Equivalences conjugating `(· + a)` to `(· + b)`
@@ -14,6 +16,8 @@ to be the type of equivalences such that `∀ x, f (x + a) = f x + b`.
1416
We also define the corresponding typeclass and prove some basic properties.
1517
-/
1618

19+
@[expose] public section
20+
1721
assert_not_exists Finset
1822

1923
open Function

‎Mathlib/Algebra/AddTorsor/Basic.lean‎

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,13 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Joseph Myers, Yury Kudryashov
55
-/
6-
import Mathlib.Algebra.AddTorsor.Defs
7-
import Mathlib.Algebra.Group.Action.Basic
8-
import Mathlib.Algebra.Group.Action.Pi
9-
import Mathlib.Algebra.Group.End
10-
import Mathlib.Algebra.Group.Pointwise.Set.Scalar
6+
module
7+
8+
public import Mathlib.Algebra.AddTorsor.Defs
9+
public import Mathlib.Algebra.Group.Action.Basic
10+
public import Mathlib.Algebra.Group.Action.Pi
11+
public import Mathlib.Algebra.Group.End
12+
public import Mathlib.Algebra.Group.Pointwise.Set.Scalar
1113

1214
/-!
1315
# Torsors of additive group actions
@@ -16,6 +18,8 @@ Further results for torsors, that are not in `Mathlib/Algebra/AddTorsor/Defs.lea
1618
increasing imports there.
1719
-/
1820

21+
@[expose] public section
22+
1923
open scoped Pointwise
2024

2125

‎Mathlib/Algebra/AddTorsor/Defs.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,9 @@ Copyright (c) 2020 Joseph Myers. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Joseph Myers, Yury Kudryashov
55
-/
6-
import Mathlib.Algebra.Group.Action.Defs
6+
module
7+
8+
public import Mathlib.Algebra.Group.Action.Defs
79

810
/-!
911
# Torsors of additive group actions
@@ -37,6 +39,8 @@ multiplicative group actions).
3739
3840
-/
3941

42+
@[expose] public section
43+
4044
assert_not_exists MonoidWithZero
4145

4246
/-- An `AddTorsor G P` gives a structure to the nonempty type `P`,

‎Mathlib/Algebra/Algebra/Basic.lean‎

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,22 +3,26 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau, Yury Kudryashov
55
-/
6-
import Mathlib.Algebra.Algebra.Defs
7-
import Mathlib.Algebra.Module.Equiv.Basic
8-
import Mathlib.Algebra.Module.Submodule.Ker
9-
import Mathlib.Algebra.Module.Submodule.RestrictScalars
10-
import Mathlib.Algebra.Module.ULift
11-
import Mathlib.Algebra.Ring.CharZero
12-
import Mathlib.Algebra.Ring.Subring.Basic
13-
import Mathlib.Data.Nat.Cast.Order.Basic
14-
import Mathlib.Data.Int.CharZero
6+
module
7+
8+
public import Mathlib.Algebra.Algebra.Defs
9+
public import Mathlib.Algebra.Module.Equiv.Basic
10+
public import Mathlib.Algebra.Module.Submodule.Ker
11+
public import Mathlib.Algebra.Module.Submodule.RestrictScalars
12+
public import Mathlib.Algebra.Module.ULift
13+
public import Mathlib.Algebra.Ring.CharZero
14+
public import Mathlib.Algebra.Ring.Subring.Basic
15+
public import Mathlib.Data.Nat.Cast.Order.Basic
16+
public import Mathlib.Data.Int.CharZero
1517

1618
/-!
1719
# Further basic results about `Algebra`.
1820
1921
This file could usefully be split further.
2022
-/
2123

24+
@[expose] public section
25+
2226
universe u v w u₁ v₁
2327

2428
open Function

0 commit comments

Comments
 (0)