Theorems · Theorem · field theory

IntermediateField.finiteDimensional_adjoin

∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {S : Set L} [Finite ↑S],
  (∀ x ∈ S, IsIntegral K x) → FiniteDimensional K ↥(IntermediateField.adjoin K S)

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.

Defined in

Mathlib.FieldTheory.IntermediateField.Adjoin.Basic

Cited by

7 results in Mathlib

Foundations

Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebraFinite