fix: add imports now needed in Imo1998Q2 and Imo1988Q6 (#11535)

Fixes breakage from #11507.
leanprover-community · Mar 20, 2024 · a584fa1 · a584fa1
1 parent 01017f4
commit a584fa1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/Archive/Imo/Imo1988Q6.lean b/Archive/Imo/Imo1988Q6.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
+import Mathlib.Algebra.Order.WithZero
 import Mathlib.Data.Nat.Prime
 import Mathlib.Data.Rat.Defs
 import Mathlib.Order.WellFounded

diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.Algebra.BigOperators.Order
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Int.Parity
 import Mathlib.GroupTheory.GroupAction.Ring