Commit 2025-01-27 09:35 36e9a271
View on Github →feat(RingTheory/IntegralClosure): prove Module.Finite R (adjoin R S) for finite set S of integral elements (#20970)
Prove that Algebra.adjoin R S has finite rank over R when S is finite with elements that are all integral over R.
Special case for singleton included.