Def ContinuousLinearMap.toLinearMap₁₂

Modification history

2026-08-03 21:26

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

feat(Topology/Algebra/Module/Spaces/ContinuousLinearMap): convert `toLinearMap₁₂` to a linear map (#41731) …

Modified ContinuousLinearMap.toLinearMap₁₂ View on Github →

2026-03-31 20:10

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

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

Modified ContinuousLinearMap.toLinearMap₁₂ View on Github →

2025-07-30 09:29

Mathlib/Topology/Algebra/Module/StrongTopology.lean

refactor: Rename ContinuousLinearMap.toLinearMap₂ (#27574) …

Added ContinuousLinearMap.toLinearMap₁₂ View on Github →