Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-04 19:56 475a669a

View on Github →

feat(topology/algebra/multilinear): define continuous multilinear maps (#1948)

Estimated changes

Modified src/linear_algebra/multilinear.lean

modified theorem multilinear_map.map_smul

Created src/topology/algebra/multilinear.lean

added theorem continuous_multilinear_map.add_apply

added theorem continuous_multilinear_map.cons_add

added theorem continuous_multilinear_map.cons_smul

added theorem continuous_multilinear_map.ext

added theorem continuous_multilinear_map.map_add

added theorem continuous_multilinear_map.map_add_univ

added theorem continuous_multilinear_map.map_coord_zero

added theorem continuous_multilinear_map.map_piecewise_add

added theorem continuous_multilinear_map.map_piecewise_smul

added theorem continuous_multilinear_map.map_smul

added theorem continuous_multilinear_map.map_smul_univ

added theorem continuous_multilinear_map.map_sub

added theorem continuous_multilinear_map.map_zero

added theorem continuous_multilinear_map.neg_apply

added theorem continuous_multilinear_map.smul_apply

added theorem continuous_multilinear_map.sub_apply

added def continuous_multilinear_map.to_continuous_linear_map

added def continuous_multilinear_map.to_multilinear_map_linear

added theorem continuous_multilinear_map.zero_apply

added structure continuous_multilinear_map