Theorem Submonoid.fg_eqLocusM

Modification history

2025-10-31 09:48
Mathlib/GroupTheory/Finiteness.lean
feat(GroupTheory/Finiteness): well-quasi-ordered monoid must be finitely generated (#30866) …
Added Submonoid.fg_eqLocusMView on Github →