update mathlib

dwrensha · Nov 16, 2024 · a0b19cb · a0b19cb
1 parent c4517c7
commit a0b19cb
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/Compfiles/Imo1969P1.lean b/Compfiles/Imo1969P1.lean
@@ -6,7 +6,7 @@ Authors: Kevin Lacker
 import Mathlib.Algebra.Ring.Identities
 import Mathlib.Data.Int.NatPrime
 import Mathlib.Tactic.Linarith
-import Mathlib.Data.Set.Finite
+import Mathlib.Data.Set.Finite.Basic
 
 import ProblemExtraction
 

diff --git a/Compfiles/Imo2008P2.lean b/Compfiles/Imo2008P2.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Manuel Candales
 -/
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Set.Finite
+import Mathlib.Data.Set.Finite.Lattice
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Abel
 import Mathlib.Tactic.Linarith

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0b70c3228f4c850c2188bfa1fd8296e246ae4f24",
+   "rev": "6270f3467257beb5cf5118e21a98a0734356657e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",