mathlib3

71150516 - chore(algebra/algebra/basic): remove a duplicate lemma (#18415)

chore(algebra/algebra/basic): remove a duplicate lemma (#18415) This combines `submodule.span_eq_restrict_scalars` (which was stated backwards and added in #6098) with `algebra.span_restrict_scalars_eq_span_of_surjective` (which was in an odd namespace, and added in #13042). The two lemmas were identical modulo argument order and explicitness. This also has the bonus of reducing the imports of `algebra.algebra.basic`.