Commit 2020-10-05 17:20 e89d0edd

View on Github →

chore(*/multilinear): generalize comp_linear_map to a family of linear maps (#4408) Together with #4316 this will give us multilinear maps corresponding to monomials.

Estimated changes

Modified src/analysis/calculus/times_cont_diff.lean

Modified src/analysis/normed_space/bounded_linear_maps.lean

Modified src/linear_algebra/multilinear.lean

modified def multilinear_map.comp_linear_map

added theorem multilinear_map.comp_linear_map_apply

Modified src/logic/function/basic.lean

added theorem function.apply_update

Modified src/topology/algebra/multilinear.lean

added theorem continuous_multilinear_map.comp_continuous_linear_map_apply