Commit 2025-10-24 16:40 a0a0b57f
View on Github →feat(GroupTheory/Finiteness): submonoid finiteness from well-quasi-order, Gordan's lemma (#30840)
We show that in a monoid whose algebraic order is a well-quasi-order (typical example is ℕ ^ k), any subtractive submonoid is finitely generated. As a corollary, AddMonoidHom.eqLocusM f g is finitely generated, which is also known as a version of Gordan's lemma when specialized for ℕ ^ k.