Def continuous_multilinear_map.to_multilinear_map_linear

Modification history

2021-01-27 08:41
src/topology/algebra/multilinear.lean
chore(*): add more simp lemmas, refactor theorems about `fintype.sum` (#5888) …
Modified continuous_multilinear_map.to_multilinear_map_linearView on Github →
2020-05-30 16:24
src/topology/algebra/multilinear.lean
refactor(algebra/module): change module into an abbreviation for semimodule (#2848) …
Modified continuous_multilinear_map.to_multilinear_map_linearView on Github →
2020-02-04 19:56
src/topology/algebra/multilinear.lean
feat(topology/algebra/multilinear): define continuous multilinear maps (#1948)
Added continuous_multilinear_map.to_multilinear_map_linearView on Github →