mathlib
f1e27d29 - feat(linear_algebra/finsupp): mem_supr_iff_exists_finset (#8268)

Commit

4 years ago

feat(linear_algebra/finsupp): mem_supr_iff_exists_finset (#8268) This is an `iff` version of `exists_finset_of_mem_supr`

Author

eric-wieser

Parents