Commit 2021-05-03 21:31 37735250View 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.
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