Commit 2023-02-11 10:50 71150516
View on Github →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.