Commit 2024-12-05 08:47 ea266590

feat(RingTheory/Algebraic): transitivity of algebraicity (#19660) Main results:

• Subalgebra.algebraicClosure: If R is a domain and S is an arbitrary R-algebra, then the elements of S that are algebraic over R form a subalgebra. (The proofs are due to Matthé van der Lee on MathOverflow.)
• Algebra.IsAlgebraic.trans': If A/S/R is a tower of algebras and both A/S and S/R are algebraic, then A/R is also algebraic, provided that S has no zero divisors and algebraMap S A is injective (so S can be regarded as an R-subalgebra of A).
• Transcendental.extendScalars: an element of an R-algebra that is transcendental over R remains transcendental over any algebraic R-subalgebra that has no zero divisors.
• IsLocalization.isAlgebraic: a localization of a nontrivial commutative ring is always algebraic. Used to golf exists_integral_multiples. Auxiliary result:
• IsAlgebraic.iff_exists_smul_integral: If R is reduced and S is an R-algebra with injective algebraMap, then an element of S is algebraic over R iff some R-multiple is integral over R.