Commit 2025-09-21 20:41 103f096e

feat(Algebra): add mem_closure_iff_of_fintype and mem_closure_finset' (#29793) mem_closure_iff_of_fintype is a corollary of mem_closure_range_iff_of_fintype, when we have a s : Set M with a Fintype s instance on it. mem_closure_finset' is a special case of mem_closure_iff_of_fintype when we have a Finset. Also add mem_span_iff_of_fintype for Submodule. Thanks for the discussion in Zulip.