Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-03 15:50 9851a886

View on Github →

feat(*/multilinear): define (continuous_)multilinear_map.restrict_scalars (#4872) I'm going to use these definitions to prove times_cont_diff_at.restrict_scalars etc.

Estimated changes

Modified src/analysis/normed_space/multilinear.lean

added theorem continuous_multilinear_map.continuous_restrict_scalars

added theorem continuous_multilinear_map.norm_restrict_scalars

modified theorem continuous_multilinear_map.op_norm_smul_le

added def continuous_multilinear_map.restrict_scalars_linear

Modified src/linear_algebra/multilinear.lean

added theorem multilinear_map.coe_restrict_scalars

added def multilinear_map.restrict_scalars

modified theorem multilinear_map.smul_apply

Modified src/topology/algebra/multilinear.lean

modified theorem continuous_linear_map.comp_continuous_multilinear_map_coe

added theorem continuous_multilinear_map.coe_restrict_scalars

added def continuous_multilinear_map.restrict_scalars

modified theorem continuous_multilinear_map.smul_apply