Mathlib Changelog
v4
Changelog
About
Github
Theorem
Submodule.mem_span_iff_exists_finset_subset
Modification history
2025-04-02 10:55
Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
feat: characterise elements of the submonoid generated by a finset (#23488) …
Added
Submodule.mem_span_iff_exists_finset_subset
View on Github →