English
Let R, S be rings with S algebraic over R, and A an algebra over S. If every element of S is algebraic over R and every element of A is algebraic over S, then every element of A is algebraic over R.
Русский
Пусть R, S — кольца, S алгебра над R, и A — алгебра над S. Если каждый элемент S алгебрачен над R, и каждый элемент A алгебрачен над S, то каждый элемент A алгебрачен над R.
LaTeX
$$$\text{IsAlgebraic}(R,S) \land \text{IsAlgebraic}(S,A) \Rightarrow \text{IsAlgebraic}(R,A).$$$
Lean4
/-- Transitivity of algebraicity for algebras over domains. -/
@[stacks 09GJ]
theorem trans [Algebra.IsAlgebraic R S] [alg : Algebra.IsAlgebraic S A] : Algebra.IsAlgebraic R A :=
⟨fun _ ↦ (alg.1 _).restrictScalars _⟩
