trans_isAlgebraic — Mathlib

English

If S is integral over R and A is algebraic over S, then A is algebraic over R.

Русский

Если S целочисленно над R и A алгебраически над S, то A алгебраично над R.

LaTeX

$$$[\text{IsIntegral}(R,S)] \land [\text{IsAlgebraic}(S,A)] \Rightarrow [\text{IsAlgebraic}(R,A)].$$$

Lean4

theorem trans_isAlgebraic [Algebra.IsIntegral R S] [alg : Algebra.IsAlgebraic S A] : Algebra.IsAlgebraic R A :=
  ⟨fun _ ↦ (alg.1 _).restrictScalars_of_isIntegral _⟩

Похожие утверждения