Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@RemyDegenne
RemyDegenne committed Nov 16, 2024
1 parent 9fcf608 commit a2eca88
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion TestingLowerBounds/FDiv/DivFunction/CurvatureMeasure.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit a2eca88

Please sign in to comment.