mathlib

09b4bfc9 - feat(linear_algebra/multilinear/basic): multilinear maps with respect to an empty family are all constant (#10433)

feat(linear_algebra/multilinear/basic): multilinear maps with respect to an empty family are all constant (#10433) This seemingly-innocuous statement is valuable as a base case for induction. Formalized as part of the Sphere Eversion project.