mathlib3

37735250 - feat(ring_theory/finiteness): add lemmas (#7409)

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.