From 473b1f0a5d63bdba29e9222976b2e4bc44483b24 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 29 Oct 2024 09:35:10 +0100 Subject: [PATCH] chore: reduce imports --- Mathlib/Testing/Plausible/Functions.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Testing/Plausible/Functions.lean b/Mathlib/Testing/Plausible/Functions.lean index 8640cf629b5e3..0599f83b053c8 100644 --- a/Mathlib/Testing/Plausible/Functions.lean +++ b/Mathlib/Testing/Plausible/Functions.lean @@ -6,7 +6,6 @@ Authors: Simon Hudon import Mathlib.Algebra.Order.Group.Nat import Mathlib.Data.Int.Range import Mathlib.Data.List.Perm.Lattice -import Mathlib.Data.List.Range import Mathlib.Data.List.Sigma import Plausible.Functions