Commit 2024-01-06 09:51 90bee82a

feat: generalize Module.Finite.trans (#9380) Add span_eq_closure and closure_induction which say that Submodule.span R s is generated by R • s as an AddSubmonoid. I feel that the existing span_induction should be replaced by closure_induction as the latter is stronger, and allow us to remove the commutativity condition in span_smul_of_span_eq_top in Algebra/Tower and generalize Module.Finite.trans to allow a non-commutative base ring.