Theorem AddSubmonoid.fg_of_subtractive

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_of_subtractiveView on Github →