feat(linear_algebra/span): add `finite_span_is_compact_element` (#13901)
feat(linear_algebra/span): add `finite_span_is_compact_element` (#13901)

This PR adds `finite_span_is_compact_element`, which extends `singleton_span_is_compact_element` to the spans of finite subsets.
This will be useful e.g. when proving the existence of a maximal submodule of a finitely generated module.







leanprover-community/mathlib,leanprover-community/mathlib