Def ContinuousLinearMap.restrictScalarsL
Modification history
2024-08-12 20:23
Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
feat(StrongTopology): generalize `ContinuousLinearMap.restrictScalarsL` (#15285)
Modified ContinuousLinearMap.restrictScalarsLView on Github →