Theorem Submonoid.FG.exists_minimal_closure_eq

Modification history

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