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.

depends on: #7279

Estimated changes

Modified src/algebra/module/submodule.lean

added theorem submodule.mem_to_add_submonoid

Modified src/algebra/monoid_algebra.lean

added theorem add_monoid_algebra.induction_on

added def add_monoid_algebra.to_multiplicative_alg_equiv

added theorem monoid_algebra.induction_on

added def monoid_algebra.to_additive_alg_equiv

Modified src/ring_theory/finiteness.lean

added theorem add_monoid_algebra.mv_polynomial_aeval_of_surjective_of_closure

added theorem monoid_algebra.mv_polynomial_aeval_of_surjective_of_closure