Commit 2025-09-01 08:25 cab32d8d
View on Github →feat(GroupTheory/Finiteness): Monoid.FG (∀ i, M i) and Group.FG (∀ i, M i) (#28670)
following the proof of Module.Finite.pi. Also add a missing instance of Group.FG (G × G').
feat(GroupTheory/Finiteness): Monoid.FG (∀ i, M i) and Group.FG (∀ i, M i) (#28670)
following the proof of Module.Finite.pi. Also add a missing instance of Group.FG (G × G').