instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet

English

An instance ensuring separability for subfields obtained by adjoining images up to i under a tower of fields with separability assumptions.

Русский

Экземпляр, гарантирующий разложимость подполей, получаемых порождением образов до i в цепочке полей при предположении разложимости.

LaTeX

$$$$\\text{instIsSeparable}_F E_i$$$$

Lean4

instance (i : ι) : Algebra.IsSeparable (E⟮<i⟯) (E⟮<i⟯⟮b (φ i)⟯) :=
  have := Algebra.isSeparable_tower_top_of_isSeparable F (E⟮<i⟯) E
  have : IsScalarTower (E⟮<i⟯) (E⟮<i⟯⟮b (φ i)⟯) E := .of_algebraMap_eq' rfl
  Algebra.isSeparable_tower_bot_of_isSeparable _ _ E

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