finiteDimensional_adjoin — Mathlib

English

If S is a finite subset of L and every element of S is integral over K, then adjoin K S is finite dimensional over K.

Русский

Если S — конечное подмножество L и каждый его элемент интегрирован над K, то K-adjoin S конечномерно над K.

LaTeX

$$Finite S → (∀ x ∈ S, IsIntegral K x) → FiniteDimensional K (adjoin K S)$$

Lean4

/-- If `L / K` is a field extension, `S` is a finite subset of `L`, such that every element of `S`
is integral (= algebraic) over `K`, then `K(S) / K` is a finite extension.
A direct corollary of `finiteDimensional_iSup_of_finite`. -/
theorem finiteDimensional_adjoin {S : Set L} [Finite S] (hS : ∀ x ∈ S, IsIntegral K x) :
    FiniteDimensional K (adjoin K S) :=
  by
  rw [← biSup_adjoin_simple, ← iSup_subtype'']
  haveI (x : S) := adjoin.finiteDimensional (hS x.1 x.2)
  exact finiteDimensional_iSup_of_finite

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