Commit 2025-04-03 18:22 a49aef05

View on Github →

feat: the product of finitely generated monoids is finitely generated (#22932) From Toric

Estimated changes

Modified Mathlib/GroupTheory/Finiteness.lean

deleted theorem AddMonoid.fg_def

modified theorem AddMonoid.fg_iff_mul_fg

modified theorem AddSubmonoid.fg_iff_mul_fg

modified theorem Monoid.fg_iff_add_fg

added theorem Submonoid.FG.prod

Modified Mathlib/RingTheory/FiniteType.lean