Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-30 10:14 4722dd46

View on Github →

feat(ring_theory/finiteness): add add_monoid_algebra.ft_of_fg (#7265) This is from lean_liquid. We prove add_monoid_algebra.ft_of_fg: if M is a finitely generated monoid then add_monoid_algebra R M if finitely generated as R-alg. The converse is also true, but the proof is longer and I wanted to keep the PR small.

Estimated changes