Adjoining elements to form subalgebras
This file develops the basic theory of subalgebras of an R-algebra generated
by a set of elements. A basic interface for
adjoin is set up, and various
results about finitely-generated subalgebras and submodules are proved.
fg (S : subalgebra R A): A predicate saying that the subalgebra is finitely-generated as an A-algebra
adjoin, algebra, finitely-generated algebra
The image of a Noetherian R-algebra under an R-algebra map is a Noetherian ring.