Skip to content

Commit 0072a62

Browse files
j-loreauxj-loreaux
committed
chore: deprecate all remaining modules in Analysis/NormedSpace (#31913)
1 parent 8a66b01 commit 0072a62

File tree

18 files changed

+103
-0
lines changed

18 files changed

+103
-0
lines changed

‎Mathlib.lean‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1976,14 +1976,28 @@ public import Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
19761976
public import Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
19771977
public import Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
19781978
public import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
1979+
public import Mathlib.Analysis.NormedSpace.Alternating.Basic
1980+
public import Mathlib.Analysis.NormedSpace.Alternating.Curry
1981+
public import Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin
19791982
public import Mathlib.Analysis.NormedSpace.BallAction
19801983
public import Mathlib.Analysis.NormedSpace.ConformalLinearMap
1984+
public import Mathlib.Analysis.NormedSpace.Connected
19811985
public import Mathlib.Analysis.NormedSpace.DualNumber
1986+
public import Mathlib.Analysis.NormedSpace.ENormedSpace
19821987
public import Mathlib.Analysis.NormedSpace.Extend
1988+
public import Mathlib.Analysis.NormedSpace.Extr
19831989
public import Mathlib.Analysis.NormedSpace.FunctionSeries
1990+
public import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
1991+
public import Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual
1992+
public import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
19841993
public import Mathlib.Analysis.NormedSpace.HomeomorphBall
19851994
public import Mathlib.Analysis.NormedSpace.IndicatorFunction
19861995
public import Mathlib.Analysis.NormedSpace.Int
1996+
public import Mathlib.Analysis.NormedSpace.MStructure
1997+
public import Mathlib.Analysis.NormedSpace.Multilinear.Basic
1998+
public import Mathlib.Analysis.NormedSpace.Multilinear.Curry
1999+
public import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
2000+
public import Mathlib.Analysis.NormedSpace.Normalize
19872001
public import Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics
19882002
public import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
19892003
public import Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear
@@ -1992,9 +2006,12 @@ public import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
19922006
public import Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm
19932007
public import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace
19942008
public import Mathlib.Analysis.NormedSpace.OperatorNorm.Prod
2009+
public import Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm
2010+
public import Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm
19952011
public import Mathlib.Analysis.NormedSpace.Pointwise
19962012
public import Mathlib.Analysis.NormedSpace.RCLike
19972013
public import Mathlib.Analysis.NormedSpace.Real
2014+
public import Mathlib.Analysis.NormedSpace.RieszLemma
19982015
public import Mathlib.Analysis.NormedSpace.SphereNormEquiv
19992016
public import Mathlib.Analysis.ODE.Gronwall
20002017
public import Mathlib.Analysis.ODE.PicardLindelof

‎Mathlib/Analysis/NormedSpace/Alternating/Basic.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Analysis.Normed.Module.Alternating.Basic
4+
5+
deprecated_module (since := "2025-11-21")

‎Mathlib/Analysis/NormedSpace/Alternating/Curry.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Analysis.Normed.Module.Alternating.Curry
4+
5+
deprecated_module (since := "2025-11-21")

‎Mathlib/Analysis/NormedSpace/Alternating/Uncurry/Fin.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
4+
5+
deprecated_module (since := "2025-11-21")

‎Mathlib/Analysis/NormedSpace/Connected.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Analysis.Normed.Module.Connected
4+
5+
deprecated_module (since := "2025-11-21")

‎Mathlib/Analysis/NormedSpace/ENormedSpace.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Analysis.Normed.Module.ENormedSpace
4+
5+
deprecated_module (since := "2025-11-21")

‎Mathlib/Analysis/NormedSpace/Extr.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Analysis.Normed.Module.Extr
4+
5+
deprecated_module (since := "2025-11-21")

‎Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Analysis.Normed.Module.HahnBanach
4+
5+
deprecated_module (since := "2025-11-06")

‎Mathlib/Analysis/NormedSpace/HahnBanach/SeparatingDual.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
module
2+
3+
public import Mathlib.Analysis.LocallyConvex.SeparatingDual
4+
public import Mathlib.Analysis.Normed.Operator.CompleteCodomain
5+
6+
deprecated_module (since := "2025-11-06")

‎Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
module
2+
3+
public import Mathlib.Analysis.LocallyConvex.Separation
4+
5+
deprecated_module (since := "2025-11-06")

0 commit comments

Comments
 (0)