Theorem Submonoid.isMulFG_top_iff

Modification history

2026-09-15 15:39
Mathlib/GroupTheory/Finiteness.lean
feat(GroupTheory/Finiteness): add general `IsMulFG` (#43532) …
Added Submonoid.isMulFG_top_iffView on Github →