instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet

English

For each i, the subfield obtained by adjoining the images up to i is finite dimensional over F.

Русский

Для каждого i подполе, порождаемое образами до i, имеет конечную размерность над F.

LaTeX

$$$$\\text{FiniteDimensional}_F(\\text{adjoin}_F(\\text{image up to } i))$$$$

Lean4

instance (i : ι) : FiniteDimensional (E⟮<i⟯) (E⟮<i⟯⟮b (φ i)⟯) :=
  adjoin.finiteDimensional ((Algebra.IsAlgebraic.tower_top (K := F) _).isAlgebraic _).isIntegral

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