Adjoining elements to form subalgebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file develops the basic theory of finitely-generated subalgebras.
fg (S : subalgebra R A) : A predicate saying that the subalgebra is finitely-generated
as an A-algebra
adjoin, algebra, finitely-generated algebra
S is finitely generated if there exists
t : finset A such that
algebra.adjoin R t = S.
The image of a Noetherian R-algebra under an R-algebra map is a Noetherian ring.