We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
lake exe mk_all
1 parent 6a56042 commit e91a22aCopy full SHA for e91a22a
1 file changed
Mathlib.lean
@@ -4954,7 +4954,6 @@ public import Mathlib.MeasureTheory.Group.Pointwise
4954
public import Mathlib.MeasureTheory.Group.Prod
4955
public import Mathlib.MeasureTheory.Integral.Asymptotics
4956
public import Mathlib.MeasureTheory.Integral.Average
4957
-public import Mathlib.MeasureTheory.Integral.Average.MeanValue
4958
public import Mathlib.MeasureTheory.Integral.Bochner.Basic
4959
public import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
4960
public import Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
0 commit comments