Commit 2025-04-19 08:21 f8ab2949

View on Github →

chore: semilinearize ContinuousLinearMap.toLinearMap₂ (#24174)

Estimated changes

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

modified def ContinuousLinearMap.toLinearMap₂

modified theorem ContinuousLinearMap.toLinearMap₂_apply