mathlib

6d85ff23 - refactor(linear_algebra/finsupp): replace mem_span_iff_total (#7735)

refactor(linear_algebra/finsupp): replace mem_span_iff_total (#7735) This PR renames the existing `mem_span_iff_total` to `mem_span_image_iff_total` and the existing `span_eq_map_total` to `span_image_eq_map_total`, and replaces them with slightly simpler lemmas about sets in the module, rather than indexed families. As usual in the linear algebra library, there is tension between using sets and using indexed families, but as `span` is defined in terms of sets I think the new lemmas merit taking the simpler names. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>