mathlib3

0ddf919e - feat(ring_theory/ideal/operations): strengthen a lemma to iff and golf (#15777)

feat(ring_theory/ideal/operations): strengthen a lemma to iff and golf (#15777) + Strengthen `exists_sum_of_mem_ideal_smul_span` to iff and rename it to `mem_ideal_smul_span_iff_exists_sum'`. + Introduce a more general version `mem_ideal_smul_span_iff_exists_sum` (without the prime) that applies to any type, not just types coerced from a set; this version is stated using `set.range` instead of `set.image`. + Use the general version to golf down `finsupp_total_apply_eq_of_fintype` in the same file (this comes from reviewing PR # 15460 after it's approved) and slightly golf `ideal.finrank_quotient_map.span_eq_top` in another file (the only place in mathlib this lemma is used previously). Co-authored-by: erd1 <the.erd.one@gmail.com> Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>