From 7e04605d9fc0b21bf910d313165684a7b39ca682 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 29 Jan 2026 22:21:14 +0100 Subject: [PATCH] remove an import Mathlib --- LeanBandits/ForMathlib/Integrable.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LeanBandits/ForMathlib/Integrable.lean b/LeanBandits/ForMathlib/Integrable.lean index 8feeb38f..5a366cf3 100644 --- a/LeanBandits/ForMathlib/Integrable.lean +++ b/LeanBandits/ForMathlib/Integrable.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Rémy Degenne. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne -/ -import Mathlib +import Mathlib.Probability.IdentDistrib open ProbabilityTheory