Theorem AddSubmonoid.fg_eqLocusM

Modification history

2025-10-24 16:40
Mathlib/GroupTheory/Finiteness.lean
feat(GroupTheory/Finiteness): submonoid finiteness from well-quasi-order, Gordan's lemma (#30840) …
Added AddSubmonoid.fg_eqLocusMView on Github →