From 0cd222783c76a636ff40f144030babff94984675 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 1 Feb 2025 10:24:55 +0000 Subject: [PATCH] fix --- MathlibTest/instance_diamonds.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/MathlibTest/instance_diamonds.lean b/MathlibTest/instance_diamonds.lean index 02932d2f6192b2..1dffa9c372c1c3 100644 --- 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