From 8d2c4b948115fd6aace1236b97eb65d9cdd6470e Mon Sep 17 00:00:00 2001 From: "Anne C.A. Baanen" Date: Mon, 25 Nov 2024 14:18:54 +0100 Subject: [PATCH] shake --- Mathlib/Data/Finsupp/Defs.lean | 1 - Mathlib/Data/Finsupp/Ext.lean | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Finsupp/Defs.lean b/Mathlib/Data/Finsupp/Defs.lean index cc74d56fe7a74..617d0cefa185c 100644 --- 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 index fc184f2cf52f3..14f8617ffb6f7 100644 --- 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 /-!