Commit 2023-04-28 01:23 1a889c75

View on Github →

feat: port Topology.Algebra.Module.StrongTopology (#3684)

Estimated changes

Modified Mathlib.lean

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

added theorem ContinuousLinearMap.strongTopology.continuousSMul

added theorem ContinuousLinearMap.strongTopology.embedding_coeFn

added theorem ContinuousLinearMap.strongTopology.hasBasis_nhds_zero

added theorem ContinuousLinearMap.strongTopology.hasBasis_nhds_zero_of_basis

added theorem ContinuousLinearMap.strongTopology.t2Space

added theorem ContinuousLinearMap.strongTopology.topologicalAddGroup

added def ContinuousLinearMap.strongTopology

added theorem ContinuousLinearMap.strongUniformity.uniformAddGroup

added theorem ContinuousLinearMap.strongUniformity.uniformEmbedding_coeFn

added def ContinuousLinearMap.strongUniformity

added theorem ContinuousLinearMap.strongUniformity_topology_eq