Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_multilinear_map.to_multilinear_map_inj

Modification history

2023-04-08 18:50
src/topology/algebra/module/multilinear.lean
chore(linear_algebra/alternating,topology/algebra/module/multilinear): add a fun_like instance (#18766)
Deleted continuous_multilinear_map.to_multilinear_map_injView on Github →
2020-10-12 14:57
src/topology/algebra/multilinear.lean
feat(analysis/normed_space/multilinear): define `mk_pi_algebra` (#4316) …
Added continuous_multilinear_map.to_multilinear_map_injView on Github →