Commit 2025-11-24 19:42 d9b0d1e9

View on Github →

feat: injectivity of the map forgetting the continuity of bilinear maps (#31564)

Estimated changes

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

added theorem ContinuousLinearMap.toBilinForm_inj

added theorem ContinuousLinearMap.toBilinForm_injective

added theorem ContinuousLinearMap.toLinearMap₁₂_inj

added theorem ContinuousLinearMap.toLinearMap₁₂_injective