Commit 2021-05-03 21:31 37735250

View on Github →

feat(ring_theory/finiteness): add lemmas (#7409) I add here some preliminary lemmas to prove that a monoid is finitely generated iff the monoid algebra is.

Estimated changes

Modified src/algebra/monoid_algebra.lean

added theorem add_monoid_algebra.mem_span_support'

modified theorem add_monoid_algebra.mem_span_support

added def add_monoid_algebra.of'

added theorem add_monoid_algebra.of'_apply

Modified src/ring_theory/finiteness.lean

added theorem add_monoid_algebra.mem_adjoint_support

added theorem add_monoid_algebra.support_gen_of_gen'

added theorem add_monoid_algebra.support_gen_of_gen

added theorem monoid_algebra.mem_adjoint_support

added theorem monoid_algebra.support_gen_of_gen'

added theorem monoid_algebra.support_gen_of_gen