Skip to content

Commit 2e28db1

Browse files
committed
chore(MeasureTheory/Integral/IntegralEqImproper): remove redundant import
1 parent 56267c9 commit 2e28db1

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ public import Mathlib.MeasureTheory.Function.JacobianOneDim
1111
public import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
1212
public import Mathlib.MeasureTheory.Measure.Haar.NormedSpace
1313
public import Mathlib.MeasureTheory.Measure.Haar.Unique
14-
public import Mathlib.MeasureTheory.Integral.DominatedConvergence
1514

1615
/-!
1716
# Links between an integral and its "improper" version

0 commit comments

Comments
 (0)