ofAlgebraic — Mathlib

English

If J is algebraic over K and L is an algebraic closure of J, then L is an algebraic closure of K.

Русский

Если J является алгебраическим расширением K, а L — алгебраическое замыкание J, то L является алгебраическим замыканием K.

LaTeX

$$$\\text{If } J/K \\text{ is algebraic and } L \\text{ is an algebraic closure of } J, \\text{ then } L \\text{ is an algebraic closure of } K.$$$

Lean4

/-- If `J` is an algebraic extension of `K` and `L` is an algebraic closure of `J`, then it is
  also an algebraic closure of `K`. -/
theorem ofAlgebraic [Algebra.IsAlgebraic K J] : IsAlgClosure K L :=
  ⟨IsAlgClosure.isAlgClosed J, .trans K J L⟩

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