English
If algebra of finite type holds for AddMonoidAlgebra R M, there exists a finite set G ⊆ M such that adjoin of images of G equals top.
Русский
Если R(AddMonoidAlgebra M) конечного типа, существует конечное подмножество G ⊆ M, для которого порождающая подалгебра равна верхнему пределу.
LaTeX
$$$\\exists G: \\mathrm{Finset}(M),\\; \\operatorname{adjoin}_R\\bigl(\\mathrm{of}'_R M'' G\\bigr) = \\top$$$
Lean4
/-- An element of `MonoidAlgebra R M` is in the subalgebra generated by its support. -/
theorem mem_adjoin_support (f : MonoidAlgebra R M) : f ∈ adjoin R (of R M '' f.support) :=
by
suffices span R (of R M '' f.support) ≤ Subalgebra.toSubmodule (adjoin R (of R M '' f.support)) by
exact this (mem_span_support f)
rw [Submodule.span_le]
exact subset_adjoin
