finiteDimensional_adjoin_pair — Mathlib

English

If x and y are integral over K in L, then the intermediate field K⟮x, y⟯ is finite-dimensional over K.

Русский

Пусть x и y интегралы над K в L. Тогда K⟮x, y⟯ конечномерно над K.

LaTeX

$$$\dim_K(K⟮x,y⟯) < \infty$$$

Lean4

theorem finiteDimensional_adjoin_pair (hx : IsIntegral K x) (hy : IsIntegral K y) : FiniteDimensional K K⟮x, y⟯ :=
  by
  have := adjoin.finiteDimensional hx
  have := adjoin.finiteDimensional hy
  rw [← Set.singleton_union, adjoin_union]
  exact finiteDimensional_sup K⟮x⟯ K⟮y⟯

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