Def ContinuousLinearMap.toLinearMap₂

Modification history

2025-07-30 09:29
Mathlib/Topology/Algebra/Module/StrongTopology.lean
refactor: Rename ContinuousLinearMap.toLinearMap₂ (#27574) …
Deleted ContinuousLinearMap.toLinearMap₂View on Github →
2025-04-19 08:21
Mathlib/Topology/Algebra/Module/StrongTopology.lean
chore: semilinearize ContinuousLinearMap.toLinearMap₂ (#24174)
Modified ContinuousLinearMap.toLinearMap₂View on Github →
2024-02-01 08:56
Mathlib/Topology/Algebra/Module/StrongTopology.lean
feat(Analysis/Fourier): derivative of Fourier transform (#9773) …
Added ContinuousLinearMap.toLinearMap₂View on Github →