Mathlib Changelog
v4
Changelog
About
Github
Theorem
ContinuousLinearMap.continuous_restrictScalars
Modification history
2024-08-12 20:23
Mathlib/Topology/Algebra/Module/StrongTopology.lean
feat(StrongTopology): generalize `ContinuousLinearMap.restrictScalarsL` (#15285)
Added
ContinuousLinearMap.continuous_restrictScalars
View on Github →