Bases adapted to a subspace

A subspace of a finite-dimensional vector space is spanned by a subset of a finite basis of the ambient space. The cardinality of that subset is the dimension of the subspace. This is useful when constructions on coordinate summands must be applied to arbitrary subspaces. The construction uses Mathlib's Module.Basis.sumQuot.

theorem Submodule.exists_basis_span_image_eq {k : Type u_1} {V : Type u_2} [Field k] [AddCommGroup V] [Module k V] [Module.Finite k V] (W : Submodule k V) : ∃ (b : Module.Basis (Fin (Module.finrank k V)) k V) (s : Finset (Fin (Module.finrank k V))), span k (⇑b '' ↑s) = W ∧ s.card = Module.finrank k ↥W

A subspace of a finite-dimensional vector space is a coordinate summand for a finite basis.