Commit 2025-04-02 10:55 5b6c7ca8

View on Github →

feat: characterise elements of the submonoid generated by a finset (#23488) From Toric

Estimated changes

Modified Mathlib/Algebra/Group/Submonoid/BigOperators.lean

added theorem Submonoid.mem_closure_finset

added theorem Submonoid.mem_closure_iff_exists_finset_subset

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean

added theorem Submodule.mem_span_finset

added theorem Submodule.mem_span_iff_exists_finset_subset

deleted theorem mem_span_finset

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

Modified Mathlib/RingTheory/Adjoin/Tower.lean