mathlib
ce6a7eba - feat(linear_algebra/multilinear_map): Add `range` and `map` (#5658)

Commit
5 years ago
feat(linear_algebra/multilinear_map): Add `range` and `map` (#5658) Note that unlike `linear_map`, `range` cannot return a submodule, only a `sub_mul_action`. We also can't guarantee closure under `smul` unless the map has at least one argument, as there is nothing requiring the multilinear map of no arguments to be zero.
Author
Parents
Loading