Commit 2026-03-31 20:10 9243d59d

View on Github →

chore: split Topology.Algebra.Module.StrongTopology (#37440)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Distribution/Distribution.lean

Modified Mathlib/Analysis/LocallyConvex/Montel.lean

Modified Mathlib/Analysis/LocallyConvex/SeparatingDual.lean

Modified Mathlib/Analysis/LocallyConvex/StrongTopology.lean

Modified Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

Modified Mathlib/Analysis/Normed/Operator/Basic.lean

Modified Mathlib/Analysis/Normed/Operator/Compact.lean

Modified Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean

Modified Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean

Modified Mathlib/Topology/Algebra/Module/PointwiseConvergence.lean

Created Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean

added def ContinuousLinearMap.postcompCompactConvergenceCLM

added def ContinuousLinearMap.precompCompactConvergenceCLM

Created Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean

added def ContinuousLinearEquiv.arrowCongr

added def ContinuousLinearEquiv.arrowCongrSL

added theorem ContinuousLinearEquiv.arrowCongr_apply

added theorem ContinuousLinearEquiv.arrowCongr_symm

added def ContinuousLinearEquiv.conjContinuousAlgEquiv

added theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_apply

added theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply

added theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_refl

added theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_trans

added theorem ContinuousLinearEquiv.symm_conjContinuousAlgEquiv

added theorem ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply

added theorem ContinuousLinearMap.coe_restrictScalarsL

added theorem ContinuousLinearMap.coe_restrict_scalarsL'

added theorem ContinuousLinearMap.completeSpace

added theorem ContinuousLinearMap.continuous_of_continuous_uncurry

added theorem ContinuousLinearMap.continuous_restrictScalars

added def ContinuousLinearMap.coprodEquivL

added theorem ContinuousLinearMap.eventually_nhds_zero_mapsTo

added theorem ContinuousLinearMap.isEmbedding_postcomp

added theorem ContinuousLinearMap.isEmbedding_restrictScalars

added theorem ContinuousLinearMap.isInducing_postcomp

added theorem ContinuousLinearMap.isUniformEmbedding_postcomp

added theorem ContinuousLinearMap.isUniformEmbedding_restrictScalars

added theorem ContinuousLinearMap.isUniformEmbedding_toUniformOnFun

added theorem ContinuousLinearMap.isUniformInducing_postcomp

added theorem ContinuousLinearMap.isVonNBounded_iff

added theorem ContinuousLinearMap.isVonNBounded_image2_apply

added theorem ContinuousLinearMap.map_add₂

added theorem ContinuousLinearMap.map_neg₂

added theorem ContinuousLinearMap.map_smul₂

added theorem ContinuousLinearMap.map_smulₛₗ₂

added theorem ContinuousLinearMap.map_sub₂

added theorem ContinuousLinearMap.map_zero₂

added def ContinuousLinearMap.postcomp

added def ContinuousLinearMap.precomp

added def ContinuousLinearMap.prodL

added def ContinuousLinearMap.restrictScalarsL

added def ContinuousLinearMap.toBilinForm

added theorem ContinuousLinearMap.toBilinForm_apply

added theorem ContinuousLinearMap.toBilinForm_inj

added theorem ContinuousLinearMap.toBilinForm_injective

added def ContinuousLinearMap.toLinearMap₁₂

added theorem ContinuousLinearMap.toLinearMap₁₂_apply

added theorem ContinuousLinearMap.toLinearMap₁₂_inj

added theorem ContinuousLinearMap.toLinearMap₁₂_injective

added def ContinuousLinearMap.toSpanSingletonCLE

added theorem ContinuousLinearMap.toUniformConvergenceCLM_continuous

added theorem ContinuousLinearMap.uniformContinuous_restrictScalars

Created Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean

added def ContinuousLinearMap.postcompUniformConvergenceCLM

added def ContinuousLinearMap.precompUniformConvergenceCLM

added def ContinuousLinearMap.toUniformConvergenceCLM

added theorem ContinuousLinearMap.toUniformConvergenceCLM_apply

added theorem ContinuousLinearMap.toUniformConvergenceCLM_symm_apply

added theorem UniformConvergenceCLM.add_apply

added theorem UniformConvergenceCLM.coe_zero

added theorem UniformConvergenceCLM.completeSpace

added theorem UniformConvergenceCLM.continuousEvalConst

added theorem UniformConvergenceCLM.continuousSMul

added theorem UniformConvergenceCLM.eventually_nhds_zero_mapsTo

added theorem UniformConvergenceCLM.ext

added theorem UniformConvergenceCLM.hasBasis_nhds_zero

added theorem UniformConvergenceCLM.hasBasis_nhds_zero_of_basis

added theorem UniformConvergenceCLM.isEmbedding_coeFn

added theorem UniformConvergenceCLM.isUniformEmbedding_coeFn

added theorem UniformConvergenceCLM.isUniformEmbedding_postcomp

added theorem UniformConvergenceCLM.isUniformInducing_coeFn

added theorem UniformConvergenceCLM.isUniformInducing_postcomp

added theorem UniformConvergenceCLM.isVonNBounded_iff

added theorem UniformConvergenceCLM.isVonNBounded_image2_apply

added theorem UniformConvergenceCLM.neg_apply

added theorem UniformConvergenceCLM.nhds_zero_eq

added theorem UniformConvergenceCLM.nhds_zero_eq_of_basis

added theorem UniformConvergenceCLM.smul_apply

added theorem UniformConvergenceCLM.sub_apply

added theorem UniformConvergenceCLM.sum_apply

added theorem UniformConvergenceCLM.t2Space

added theorem UniformConvergenceCLM.tendsto_iff_tendstoUniformlyOn

added theorem UniformConvergenceCLM.topologicalSpace_eq

added theorem UniformConvergenceCLM.topologicalSpace_mono

added theorem UniformConvergenceCLM.uniformSpace_eq

added theorem UniformConvergenceCLM.uniformSpace_mono

added theorem UniformConvergenceCLM.uniformity_toTopologicalSpace_eq

added def UniformConvergenceCLM

Deleted Mathlib/Topology/Algebra/Module/StrongTopology.lean

deleted def ContinuousLinearEquiv.arrowCongr

deleted def ContinuousLinearEquiv.arrowCongrSL

deleted theorem ContinuousLinearEquiv.arrowCongr_apply

deleted theorem ContinuousLinearEquiv.arrowCongr_symm

deleted def ContinuousLinearEquiv.conjContinuousAlgEquiv

deleted theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_apply

deleted theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_apply_apply

deleted theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_refl

deleted theorem ContinuousLinearEquiv.conjContinuousAlgEquiv_trans

deleted theorem ContinuousLinearEquiv.symm_conjContinuousAlgEquiv

deleted theorem ContinuousLinearEquiv.symm_conjContinuousAlgEquiv_apply_apply

deleted theorem ContinuousLinearMap.coe_restrictScalarsL

deleted theorem ContinuousLinearMap.coe_restrict_scalarsL'

deleted theorem ContinuousLinearMap.completeSpace

deleted theorem ContinuousLinearMap.continuous_of_continuous_uncurry

deleted theorem ContinuousLinearMap.continuous_restrictScalars

deleted def ContinuousLinearMap.coprodEquivL

deleted theorem ContinuousLinearMap.eventually_nhds_zero_mapsTo

deleted theorem ContinuousLinearMap.isEmbedding_postcomp

deleted theorem ContinuousLinearMap.isEmbedding_restrictScalars

deleted theorem ContinuousLinearMap.isInducing_postcomp

deleted theorem ContinuousLinearMap.isUniformEmbedding_postcomp

deleted theorem ContinuousLinearMap.isUniformEmbedding_restrictScalars

deleted theorem ContinuousLinearMap.isUniformEmbedding_toUniformOnFun

deleted theorem ContinuousLinearMap.isUniformInducing_postcomp

deleted theorem ContinuousLinearMap.isVonNBounded_iff

deleted theorem ContinuousLinearMap.isVonNBounded_image2_apply

deleted theorem ContinuousLinearMap.map_add₂

deleted theorem ContinuousLinearMap.map_neg₂

deleted theorem ContinuousLinearMap.map_smul₂

deleted theorem ContinuousLinearMap.map_smulₛₗ₂

deleted theorem ContinuousLinearMap.map_sub₂

deleted theorem ContinuousLinearMap.map_zero₂

deleted def ContinuousLinearMap.postcomp

deleted def ContinuousLinearMap.postcompCompactConvergenceCLM

deleted def ContinuousLinearMap.postcompUniformConvergenceCLM

deleted def ContinuousLinearMap.precomp

deleted def ContinuousLinearMap.precompCompactConvergenceCLM

deleted def ContinuousLinearMap.precompUniformConvergenceCLM

deleted def ContinuousLinearMap.prodL

deleted def ContinuousLinearMap.restrictScalarsL

deleted def ContinuousLinearMap.toBilinForm

deleted theorem ContinuousLinearMap.toBilinForm_apply

deleted theorem ContinuousLinearMap.toBilinForm_inj

deleted theorem ContinuousLinearMap.toBilinForm_injective

deleted def ContinuousLinearMap.toLinearMap₁₂

deleted theorem ContinuousLinearMap.toLinearMap₁₂_apply

deleted theorem ContinuousLinearMap.toLinearMap₁₂_inj

deleted theorem ContinuousLinearMap.toLinearMap₁₂_injective

deleted def ContinuousLinearMap.toSpanSingletonCLE

deleted def ContinuousLinearMap.toUniformConvergenceCLM

deleted theorem ContinuousLinearMap.toUniformConvergenceCLM_apply

deleted theorem ContinuousLinearMap.toUniformConvergenceCLM_continuous

deleted theorem ContinuousLinearMap.toUniformConvergenceCLM_symm_apply

deleted theorem ContinuousLinearMap.uniformContinuous_restrictScalars

deleted theorem UniformConvergenceCLM.add_apply

deleted theorem UniformConvergenceCLM.coe_zero

deleted theorem UniformConvergenceCLM.completeSpace

deleted theorem UniformConvergenceCLM.continuousEvalConst

deleted theorem UniformConvergenceCLM.continuousSMul

deleted theorem UniformConvergenceCLM.eventually_nhds_zero_mapsTo

deleted theorem UniformConvergenceCLM.ext

deleted theorem UniformConvergenceCLM.hasBasis_nhds_zero

deleted theorem UniformConvergenceCLM.hasBasis_nhds_zero_of_basis

deleted theorem UniformConvergenceCLM.isEmbedding_coeFn

deleted theorem UniformConvergenceCLM.isUniformEmbedding_coeFn

deleted theorem UniformConvergenceCLM.isUniformEmbedding_postcomp

deleted theorem UniformConvergenceCLM.isUniformInducing_coeFn

deleted theorem UniformConvergenceCLM.isUniformInducing_postcomp

deleted theorem UniformConvergenceCLM.isVonNBounded_iff

deleted theorem UniformConvergenceCLM.isVonNBounded_image2_apply

deleted theorem UniformConvergenceCLM.neg_apply

deleted theorem UniformConvergenceCLM.nhds_zero_eq

deleted theorem UniformConvergenceCLM.nhds_zero_eq_of_basis

deleted theorem UniformConvergenceCLM.smul_apply

deleted theorem UniformConvergenceCLM.sub_apply

deleted theorem UniformConvergenceCLM.sum_apply

deleted theorem UniformConvergenceCLM.t2Space

deleted theorem UniformConvergenceCLM.tendsto_iff_tendstoUniformlyOn

deleted theorem UniformConvergenceCLM.topologicalSpace_eq

deleted theorem UniformConvergenceCLM.topologicalSpace_mono

deleted theorem UniformConvergenceCLM.uniformSpace_eq

deleted theorem UniformConvergenceCLM.uniformSpace_mono

deleted theorem UniformConvergenceCLM.uniformity_toTopologicalSpace_eq

deleted def UniformConvergenceCLM

Modified Mathlib/Topology/Algebra/Module/TopDualPairing.lean