Commit 2025-09-02 22:44 de299568

View on Github →

chore(Analysis/{NormedSpace,Normed/Group}): move files (#29267) This moves / renames the following files in Analysis/NormedSpace/ to Analysis/Normed/Group/

IndicatorFunction → Indicator
FunctionSeries → FunctionSeries This is part of #28698 to migrate the material in Analysis/NormedSpace/ to other locations.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/SmoothSeries.lean

Modified Mathlib/Analysis/Complex/LocallyUniformLimit.lean

Renamed Mathlib/Analysis/NormedSpace/FunctionSeries.lean to Mathlib/Analysis/Normed/Group/FunctionSeries.lean

Renamed Mathlib/Analysis/NormedSpace/IndicatorFunction.lean to Mathlib/Analysis/Normed/Group/Indicator.lean

Modified Mathlib/Analysis/NormedSpace/MultipliableUniformlyOn.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/TsumUniformlyOn.lean

Modified Mathlib/Topology/UrysohnsLemma.lean