Theorem Submonoid.FG.pi

Modification history

2025-09-01 08:25

Mathlib/GroupTheory/Finiteness.lean

feat(GroupTheory/Finiteness): `Monoid.FG (∀ i, M i)` and `Group.FG (∀ i, M i)` (#28670) …

Added Submonoid.FG.pi View on Github →