Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-11-21 13:53
312eeb7c
View on Github →
chore(Analysis/{NormedSpace,Normed/Module}): migrate all remaining files (
#30281
) closes
#28698
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Analysis/CStarAlgebra/Unitary/Span.lean
Modified
Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/CompCLM.lean
Modified
Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
Modified
Mathlib/Analysis/Calculus/IteratedDeriv/ConvergenceOnBall.lean
Modified
Mathlib/Analysis/Complex/AbsMax.lean
Modified
Mathlib/Analysis/Convex/AmpleSet.lean
Renamed
Mathlib/Analysis/NormedSpace/Alternating/Basic.lean
to
Mathlib/Analysis/Normed/Module/Alternating/Basic.lean
Renamed
Mathlib/Analysis/NormedSpace/Alternating/Curry.lean
to
Mathlib/Analysis/Normed/Module/Alternating/Curry.lean
Renamed
Mathlib/Analysis/NormedSpace/Alternating/Uncurry/Fin.lean
to
Mathlib/Analysis/Normed/Module/Alternating/Uncurry/Fin.lean
Renamed
Mathlib/Analysis/NormedSpace/Connected.lean
to
Mathlib/Analysis/Normed/Module/Connected.lean
Renamed
Mathlib/Analysis/NormedSpace/ENormedSpace.lean
to
Mathlib/Analysis/Normed/Module/ENormedSpace.lean
Renamed
Mathlib/Analysis/NormedSpace/Extr.lean
to
Mathlib/Analysis/Normed/Module/Extr.lean
Modified
Mathlib/Analysis/Normed/Module/FiniteDimension.lean
Renamed
Mathlib/Analysis/NormedSpace/MStructure.lean
to
Mathlib/Analysis/Normed/Module/MStructure.lean
Renamed
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
to
Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
Renamed
Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
to
Mathlib/Analysis/Normed/Module/Multilinear/Curry.lean
Renamed
Mathlib/Analysis/NormedSpace/MultipliableUniformlyOn.lean
to
Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean
Renamed
Mathlib/Analysis/NormedSpace/Normalize.lean
to
Mathlib/Analysis/Normed/Module/Normalize.lean
Renamed
Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
to
Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean
Renamed
Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
to
Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean
Renamed
Mathlib/Analysis/NormedSpace/RieszLemma.lean
to
Mathlib/Analysis/Normed/Module/RieszLemma.lean
Modified
Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
Modified
Mathlib/Analysis/Normed/Operator/CompleteCodomain.lean
Modified
Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean
Modified
Mathlib/Geometry/Euclidean/SignedDist.lean
Modified
Mathlib/NumberTheory/LSeries/ZMod.lean
Modified
Mathlib/NumberTheory/ModularForms/DedekindEta.lean