Theorem Submonoid.exists_minimal_closure_eq_top

Modification history

2025-05-14 14:51
Mathlib/GroupTheory/Finiteness.lean
feat: a finitely generated submonoid has a minimal generating set (#23904) …
Added Submonoid.exists_minimal_closure_eq_topView on Github →