Commit 2026-09-15 15:39 06d89b76

View on Github →

feat(GroupTheory/Finiteness): add general IsMulFG (#43532) This PR adds a general IsMulFG predicate on semigroups that generalizes all four existing definitions Monoid.FG, Submonoid.FG, Group.FG and Subgroup.FG. Ultimately the plan will be to deprecate all four existing definitions in favor of IsMulFG. Previously the subobject predicates Submonoid.FG and Subgroup.FG were used to define the more general Monoid.FG and Group.FG, but the new IsMulFG defines the general predicate directly.

Estimated changes

added theorem Finset.exists_toSet
added theorem Finset.forall_toSet
deleted theorem AddGroup.fg_def
modified theorem Group.fg_iff
modified theorem Group.fg_iff_monoid_fg
modified theorem Group.fg_iff_subgroup_fg
added theorem Group.isMulFG_iff
added theorem IsMulFG.of_surjective
added theorem Monoid.FG.fg_top
modified theorem Monoid.fg_iff_add_fg
added theorem Monoid.isMulFG_iff
added theorem Semigroup.isMulFG_iff
deleted def Subgroup.FG
added theorem Subgroup.isMulFG_iff
deleted def Submonoid.FG
added theorem Submonoid.isMulFG_iff
added theorem isAddFG_additive_iff
added theorem isMulFG_congr