Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous.prod_mapL

Modification history

2022-04-05 09:11
src/analysis/normed_space/operator_norm.lean
feat(analysis): continuous_linear_map.prod_mapL (#13165) …
Added continuous.prod_mapLView on Github →