Theorem Submonoid.mem_closure_iff_exists_finset_subset

Modification history

2025-04-02 10:55
Mathlib/Algebra/Group/Submonoid/BigOperators.lean
feat: characterise elements of the submonoid generated by a finset (#23488) …
Added Submonoid.mem_closure_iff_exists_finset_subsetView on Github →