basic): the space of multilinear maps is finite-dimensional when the components are finite-dimensional (#10504)

Commit

4 years ago

feat(linear_algebra/multilinear/basic): the space of multilinear maps is finite-dimensional when the components are finite-dimensional (#10504) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents

53533697

mathlib 892d465a - feat(linear_algebra/multilinear/basic): the space of multilinear maps is finite-dimensional when the components are finite-dimensional (#10504)

mathlib
892d465a - feat(linear_algebra/multilinear/basic): the space of multilinear maps is finite-dimensional when the components are finite-dimensional (#10504)