Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-05 09:11 01a424ba

View on Github →

feat(analysis): continuous_linear_map.prod_mapL (#13165) From the sphere eversion project, Co-authored by Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com

Estimated changes

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous.prod_mapL

added theorem continuous.prod_map_equivL

added def continuous_linear_map.prod_mapL

added theorem continuous_linear_map.prod_mapL_apply

added theorem continuous_on.prod_mapL

added theorem continuous_on.prod_map_equivL