fix

leanprover-community · Feb 1, 2025 · dbb0b7b · dbb0b7b
1 parent 055a84f
commit dbb0b7b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/Mathlib/FieldTheory/Finite/Basic.lean b/Mathlib/FieldTheory/Finite/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Joey van Langen, Casper Putz
 -/
 import Mathlib.Algebra.CharP.Reduced
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.Data.ZMod.ValMinAbs
 import Mathlib.FieldTheory.Separable
 import Mathlib.RingTheory.IntegralDomain

diff --git a/Mathlib/NumberTheory/LucasPrimality.lean b/Mathlib/NumberTheory/LucasPrimality.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Bolton Bailey. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bolton Bailey
 -/
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.RingTheory.IntegralDomain
 
 /-!