isAlgebraic_adjoin_pair — Mathlib

English

If x and y are integral over K, then the intermediate field K⟮x, y⟯ is algebraic over K; equivalently, every element of K⟮x, y⟯ is algebraic over K.

Русский

Пусть x и y интегралы над K. Тогда промежуточное поле K⟮x, y⟯ алгебраическое над K; то есть каждый элемент K⟮x, y⟯ алгебраичен над K.

LaTeX

$$$K⟮x,y⟯ / K \text{ is algebraic}$$$

Lean4

theorem isAlgebraic_adjoin_pair (hx : IsIntegral K x) (hy : IsIntegral K y) : Algebra.IsAlgebraic K K⟮x, y⟯ :=
  by
  apply IntermediateField.isAlgebraic_adjoin
  simp [hx, hy]

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