Skip to content

Commit 0671720

Browse files
committed
feat: deprecate file (#36076)
File moved in #36025.
1 parent 98cc46e commit 0671720

File tree

2 files changed

+13
-0
lines changed

2 files changed

+13
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5212,6 +5212,7 @@ public import Mathlib.MeasureTheory.Measure.AEDisjoint
52125212
public import Mathlib.MeasureTheory.Measure.AEMeasurable
52135213
public import Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
52145214
public import Mathlib.MeasureTheory.Measure.AddContent
5215+
public import Mathlib.MeasureTheory.Measure.CharacteristicFunction
52155216
public import Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
52165217
public import Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
52175218
public import Mathlib.MeasureTheory.Measure.Comap
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
module
2+
3+
public import Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
4+
public import Mathlib.Analysis.Fourier.FourierTransform
5+
public import Mathlib.Analysis.InnerProductSpace.Dual
6+
public import Mathlib.Analysis.InnerProductSpace.ProdL2
7+
public import Mathlib.Analysis.Normed.Lp.MeasurableSpace
8+
public import Mathlib.MeasureTheory.Group.IntegralConvolution
9+
public import Mathlib.MeasureTheory.Integral.Pi
10+
public import Mathlib.MeasureTheory.Measure.FiniteMeasureExt
11+
12+
deprecated_module (since := "2026-03-03")

0 commit comments

Comments
 (0)