From a2eca883389912c7e2d3156854d9ecdfcce1a280 Mon Sep 17 00:00:00 2001 From: RemyDegenne Date: Sat, 16 Nov 2024 17:43:27 +0100 Subject: [PATCH] fix --- TestingLowerBounds/FDiv/DivFunction/CurvatureMeasure.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestingLowerBounds/FDiv/DivFunction/CurvatureMeasure.lean b/TestingLowerBounds/FDiv/DivFunction/CurvatureMeasure.lean index 1d59e711..e36c023b 100644 --- a/TestingLowerBounds/FDiv/DivFunction/CurvatureMeasure.lean +++ b/TestingLowerBounds/FDiv/DivFunction/CurvatureMeasure.lean @@ -8,7 +8,7 @@ import Mathlib.MeasureTheory.Constructions.Polish.Basic import Mathlib.MeasureTheory.Integral.FundThmCalculus import TestingLowerBounds.Sorry.ByParts import TestingLowerBounds.ForMathlib.LeftRightDeriv -import TestingLowerBounds.FDiv.DivFunction.Basic +import TestingLowerBounds.FDiv.DivFunction.RightDeriv open MeasureTheory Set StieltjesFunction Function Filter