Commit 2021-06-03 07:38 6d85ff23

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.