shake

leanprover-community · Nov 25, 2024 · 8d2c4b9 · 8d2c4b9
1 parent 890c963
commit 8d2c4b9
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean
@@ -6,7 +6,6 @@ Authors: Johannes Hölzl, Kim Morrison
 import Mathlib.Algebra.Group.Indicator
 import Mathlib.Data.Finset.Max
 import Mathlib.Data.Set.Finite.Basic
-import Mathlib.Algebra.Group.TypeTags.Hom
 
 /-!
 # Type of functions with finite support

diff --git a/Mathlib/Data/Finsupp/Ext.lean b/Mathlib/Data/Finsupp/Ext.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kim Morrison
 -/
 import Mathlib.Algebra.Group.Submonoid.Basic
+import Mathlib.Algebra.Group.TypeTags.Hom
 import Mathlib.Data.Finsupp.Defs
 
 /-!