Theorem Submonoid.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) …
Modified Submonoid.FG.prodView on Github →
2025-04-03 18:22
Mathlib/GroupTheory/Finiteness.lean
feat: the product of finitely generated monoids is finitely generated (#22932) …
Added Submonoid.FG.prodView on Github →