trans_isIntegral — Mathlib

English

If R ⊆ S with S 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_isIntegral [Algebra.IsAlgebraic R S] [int : Algebra.IsIntegral S A] : Algebra.IsAlgebraic R A :=
  ⟨fun _ ↦ (int.1 _).trans_isAlgebraic _⟩

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