Theorem Subgroup.FG.prod

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 Subgroup.FG.prod View on Github →