Theorem CommMonoid.fg_of_wellQuasiOrderedLE

Modification history

2026-09-15 15:39
Mathlib/GroupTheory/Finiteness.lean
feat(GroupTheory/Finiteness): add general `IsMulFG` (#43532) …
Modified CommMonoid.fg_of_wellQuasiOrderedLEView on Github →
2025-10-31 09:48
Mathlib/GroupTheory/Finiteness.lean
feat(GroupTheory/Finiteness): well-quasi-ordered monoid must be finitely generated (#30866) …
Added CommMonoid.fg_of_wellQuasiOrderedLEView on Github →