Skip to content

Commit 25f59b4

Browse files
committed
Bump mathlib
1 parent 0c1435b commit 25f59b4

File tree

5 files changed

+57
-16
lines changed

5 files changed

+57
-16
lines changed

LeanCamCombi.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@ import LeanCamCombi.Kneser.KneserRuzsa
2424
import LeanCamCombi.Kneser.MulStab
2525
import LeanCamCombi.LittlewoodOfford
2626
import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
27-
import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
2827
import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
2928
import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
3029
import LeanCamCombi.Mathlib.Analysis.Convex.Independence

LeanCamCombi/GrowthInGroups/VerySmallDoubling.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ import Mathlib.Data.Set.Card
1010
import Mathlib.Tactic.Linarith
1111
import Mathlib.Tactic.Qify
1212
import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
13-
import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
1413
import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
1514

1615
open Finset MulOpposite

LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

Lines changed: 0 additions & 7 deletions
This file was deleted.

lake-manifest.json

Lines changed: 56 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "500a529408399c44d7e1649577e3c98697f95aa4",
8+
"rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
99
"name": "batteries",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "main",
@@ -25,7 +25,7 @@
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "leanprover-community",
28-
"rev": "9ac12945862fa39eab7795c2f79bb9aa0c8e332c",
28+
"rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
2929
"name": "aesop",
3030
"manifestFile": "lake-manifest.json",
3131
"inputRev": "master",
@@ -35,10 +35,10 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "leanprover-community",
38-
"rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
38+
"rev": "23268f52d3505955de3c26a42032702c25cfcbf8",
3939
"name": "proofwidgets",
4040
"manifestFile": "lake-manifest.json",
41-
"inputRev": "v0.0.43",
41+
"inputRev": "v0.0.44",
4242
"inherited": true,
4343
"configFile": "lakefile.lean"},
4444
{"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
5555
"type": "git",
5656
"subDir": null,
5757
"scope": "leanprover-community",
58-
"rev": "c1970bea80ac3357a6a991a6d00d12e7435c12c7",
58+
"rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
5959
"name": "importGraph",
6060
"manifestFile": "lake-manifest.json",
6161
"inputRev": "main",
@@ -71,15 +71,65 @@
7171
"inputRev": "main",
7272
"inherited": true,
7373
"configFile": "lakefile.toml"},
74+
{"url": "https://github.com/leanprover-community/plausible",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "d212dd74414e997653cd3484921f4159c955ccca",
79+
"name": "plausible",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
7484
{"url": "https://github.com/leanprover-community/mathlib4.git",
7585
"type": "git",
7686
"subDir": null,
7787
"scope": "",
78-
"rev": "348232e527e0363cd27a7a49302dad2de3817be6",
88+
"rev": "df174a8a32fb9b7661ec4faa48a6a6a6bb4cf0d5",
7989
"name": "mathlib",
8090
"manifestFile": "lake-manifest.json",
8191
"inputRev": null,
8292
"inherited": false,
93+
"configFile": "lakefile.lean"},
94+
{"url": "https://github.com/acmepjz/md4lean",
95+
"type": "git",
96+
"subDir": null,
97+
"scope": "",
98+
"rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
99+
"name": "MD4Lean",
100+
"manifestFile": "lake-manifest.json",
101+
"inputRev": "main",
102+
"inherited": true,
103+
"configFile": "lakefile.lean"},
104+
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
105+
"type": "git",
106+
"subDir": null,
107+
"scope": "",
108+
"rev": "107e98b3e7603628d9bfd817b4704488d8a25e96",
109+
"name": "UnicodeBasic",
110+
"manifestFile": "lake-manifest.json",
111+
"inputRev": "main",
112+
"inherited": true,
113+
"configFile": "lakefile.lean"},
114+
{"url": "https://github.com/dupuisf/BibtexQuery",
115+
"type": "git",
116+
"subDir": null,
117+
"scope": "",
118+
"rev": "bdc2fc30b1e834b294759a5d391d83020a90058e",
119+
"name": "BibtexQuery",
120+
"manifestFile": "lake-manifest.json",
121+
"inputRev": "master",
122+
"inherited": true,
123+
"configFile": "lakefile.lean"},
124+
{"url": "https://github.com/leanprover/doc-gen4",
125+
"type": "git",
126+
"subDir": null,
127+
"scope": "",
128+
"rev": "c2156beadb1a4d049ff3b19fe396c5403025aac5",
129+
"name": "«doc-gen4»",
130+
"manifestFile": "lake-manifest.json",
131+
"inputRev": "main",
132+
"inherited": false,
83133
"configFile": "lakefile.lean"}],
84134
"name": "LeanCamCombi",
85135
"lakeDir": ".lake"}

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.13.0-rc3
1+
leanprover/lean4:v4.13.0

0 commit comments

Comments
 (0)