fix

leanprover-community · Feb 1, 2025 · 0cd2227 · 0cd2227
1 parent dbb0b7b
commit 0cd2227
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/MathlibTest/instance_diamonds.lean b/MathlibTest/instance_diamonds.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.EuclideanDomain.Field
+import Mathlib.Algebra.Field.ZMod
 import Mathlib.Algebra.GroupWithZero.Action.Prod
 import Mathlib.Algebra.GroupWithZero.Action.Units
 import Mathlib.Algebra.Module.Pi