mathlib
d7b5ffa0 - chore(linear_algebra/multilinear): add const_of_is_empty (#10291)

Commit

4 years ago

chore(linear_algebra/multilinear): add const_of_is_empty (#10291) This is extracted from `pi_tensor_product.is_empty_equiv`

Author

eric-wieser

Parents