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