Theorems · Theorem · group theory

AddSubmonoid.fg_eqLocusM

∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M]
  [IsOrderedCancelAddMonoid M] [CanonicallyOrderedAdd M] [inst_5 : AddMonoid N] [IsCancelAdd N] (f g : M →+ N),
  (f.eqLocusM g).FG

If f g are homomorphisms from a canonically ordered and well-quasi-ordered additive monoid M to a cancellative additive monoid N, the submonoid of M on which f and g agree is finitely generated. When M and N are ℕ ^ k, this is also known as a version of Gordan's lemma.

Defined in

Mathlib.GroupTheory.Finiteness

Cited by

0 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidPartialOrderWellQuasiOrderedLEIsOrderedCancelAddMonoidCanonicallyOrderedAddAddMonoidIsCancelAdd