Theorem ContinuousLinearMap.toUniformConvergenceCLM_symm_apply

Modification history

2026-03-31 20:10

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

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

Modified ContinuousLinearMap.toUniformConvergenceCLM_symm_apply View on Github →

2025-11-19 00:44

Mathlib/Topology/Algebra/Module/StrongTopology.lean

feat(Topology/Algebra): the equivalence of continuous linear maps and `UniformConvergenceCLM` (#31756)

Added ContinuousLinearMap.toUniformConvergenceCLM_symm_apply View on Github →