Finitely generated module

Finitely generated module over a module-finite -monoid

Let be a Module-finite -monoid and be a finitely generated -module. Then is a finitely generated -module. #m/thm/module

Prove

Let be an -spanning set for and be a -spanning set for . Then

is an -spanning set for , since any may be expressed as an -linear combination of 's and the coëfficients may then be expressed as linear combinations of 's.

#state/tidy | #lang/en | #SemBr