Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 09:30 251a42b5

View on Github →

feat(ring_theory/finiteness): add monoid_algebra.ft_iff_fg (#7445) We prove here add monoid_algebra.ft_iff_fg: the monoid algebra is of finite type if and only if the monoid is finitely generated.

depends on: #7409

Estimated changes

Modified src/algebra/monoid_algebra.lean

added theorem add_monoid_algebra.of'_eq_of

Modified src/ring_theory/finiteness.lean

added theorem add_monoid_algebra.exists_finset_adjoin_eq_top

added theorem add_monoid_algebra.fg_of_finite_type

added theorem add_monoid_algebra.finite_type_iff_fg

added theorem add_monoid_algebra.mem_adjoin_support

deleted theorem add_monoid_algebra.mem_adjoint_support

added theorem add_monoid_algebra.mem_closure_of_mem_span_closure

added theorem add_monoid_algebra.of'_mem_span

added theorem monoid_algebra.exists_finset_adjoin_eq_top

added theorem monoid_algebra.fg_of_finite_type

added theorem monoid_algebra.finite_type_iff_fg

modified theorem monoid_algebra.mem_adjoint_support

added theorem monoid_algebra.mem_closure_of_mem_span_closure

added theorem monoid_algebra.of_mem_span_of_iff