Commit 2025-10-31 09:48 5ebeef0d
View on Github →feat(GroupTheory/Finiteness): well-quasi-ordered monoid must be finitely generated (#30866) This is a trivial corollary that I forgot to add in #30840. Not an instance, since well-quasi-order is much stronger than finitely generated. Also generalize the results in #30840 to multiplicative monoids.