Commit 2020-10-13 16:46 b1c1033f
View on Github →feat(analysis/normed_space/operator_norm): construct a continuous_linear_equiv from a linear_equiv and bounds in both directions (#4583)
feat(analysis/normed_space/operator_norm): construct a continuous_linear_equiv from a linear_equiv and bounds in both directions (#4583)